dblp.uni-trier.dewww.dagstuhl.dewww.uni-trier.de

K. Rustan M. Leino Home Page Coauthor index pubzone.org

List of publications from the DBLP Bibliography Server - FAQ
Ask others: ACM DL/Guide - CiteSeerX - CSB - MetaPress - Google - Bing - Yahoo

DBLP keys2012
84Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Automating Induction with an SMT Solver. VMCAI 2012: 315-331
83Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Developing Verified Programs with Dafny. VSTTE 2012: 82
2011
82Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLParosh Aziz Abdulla, K. Rustan M. Leino: Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings Springer 2011
81Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLVladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß: The 1st Verified Software Competition: Experience Report. FM 2011: 154-168
80Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: From Retrospective Verification to Forward-Looking Development. NASA Formal Methods 2011: 1
79Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLClaire Le Goues, K. Rustan M. Leino, Michal Moskal: The Boogie Verification Debugger (Tool Paper). SEFM 2011: 407-414
78Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLMike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, Herman Venter: Specification and verification: the Spec# experience. Commun. ACM 54(6): 81-91 (2011)
2010
77Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Peter Müller, Jan Smans: Deadlock-Free Channels and Locks. ESOP 2010: 407-426
76Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Dafny: An Automatic Program Verifier for Functional Correctness. LPAR (Dakar) 2010: 348-370
75Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Philipp Rümmer: A Polymorphic Intermediate Verification Language: Design and Logical Encoding. TACAS 2010: 312-327
74Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Tools and Behavioral Abstraction: A Direction for Software Engineering. The Future of Software Engineering 2010: 115-124
73Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Verifying Concurrent Programs with Chalice. VMCAI 2010: 2
72Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Rosemary Monahan: Dafny Meets the Verification Benchmarks Challenge. VSTTE 2010: 112-126
71Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLMichael Barnett, K. Rustan M. Leino: To Goto Where No Statement Has Gone Before. VSTTE 2010: 157-168
70Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Learning to do program verification. Commun. ACM 53(6): 106 (2010)
69Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLJochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies: Doomed program points. Formal Methods in System Design 37(2-3): 171-199 (2010)
2009
68Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Peter Müller: A Basis for Verifying Multi-threaded Programs. ESOP 2009: 378-393
67Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Ronald Middelkoop: Proving Consistency of Pure Methods and Model Fields. FASE 2009: 231-245
66Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLJochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies: It's Doomed; We Can Prove It. FM 2009: 338-353
65Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Peter Müller, Jan Smans: Verification of Concurrent Programs with Chalice. FOSAD 2009: 195-222
64Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Rosemary Monahan: Reasoning about comprehensions with first-order SMT solvers. SAC 2009: 615-622
2008
63Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software Engineering. COMPSAC 2008: 11
62Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Peter Müller: Verification of Equivalent-Results Methods. ESOP 2008: 307-321
61Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Angela Wallenburg: Class-local object invariants. ISEC 2008: 57-66
60Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Peter Müller: Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs. LASER Summer School 2008: 91-139
59Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLSascha Böhme, K. Rustan M. Leino, Burkhart Wolff: HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier. TPHOLs 2008: 150-166
58Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Peter Müller, Angela Wallenburg: Flexible Immutability with Frozen Objects. VSTTE 2008: 192-208
57Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLBart Jacobs, Frank Piessens, Jan Smans, K. Rustan M. Leino, Wolfram Schulte: A programming model for concurrent object-oriented programs. ACM Trans. Program. Lang. Syst. 31(1): (2008)
2007
56Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Specifying and verifying software. ASE 2007: 2
55Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Designing Verification Conditions for Software. CADE 2007: 345
54Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Wolfram Schulte: Using History Invariants to Verify Observers. ESOP 2007: 80-94
53Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLÁdám Darvas, K. Rustan M. Leino: Practical Reasoning About Invocations and Implementations of Pure Methods. FASE 2007: 336-351
52Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Verifying Object-Oriented Software: Lessons and Challenges. TACAS 2007: 2
51Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLGary T. Leavens, K. Rustan M. Leino, Peter Müller: Specification and verification challenges for sequential object-oriented programs. Formal Asp. Comput. 19(2): 159-189 (2007)
2006
50Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Peter Müller: A Verification Methodology for Model Fields. ESOP 2006: 115-130
49Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Specifying and Verifying Programs in Spec#. Ershov Memorial Conference 2006: 20
2005
48Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Francesco Logozzo: Loop Invariants on Demand. APLAS 2005: 119-134
47Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Program Verification and Programming Methodology. Abstract State Machines 2005: 73
46Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Peter Müller: Modular Verification of Static Class Invariants. FM 2005: 26-42
45Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLMichael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, K. Rustan M. Leino: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. FMCO 2005: 364-387
44Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLMichael Barnett, K. Rustan M. Leino: Weakest-precondition of unstructured programs. PASTE 2005: 82-87
43Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLBart Jacobs, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte: Safe Concurrency for Aggregate Objects with Invariants. SEFM 2005: 137-147
42Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Invariants on Demand. SEFM 2005: 148-149
41Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Madan Musuvathi, Xinming Ou: A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover. TACAS 2005: 334-348
40Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLBor-Yuh Evan Chang, K. Rustan M. Leino: Abstract Interpretation with Alien Expressions and Heap Structures. VMCAI 2005: 147-163
39Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLMichael Barnett, Robert DeLine, Manuel Fähndrich, Bart Jacobs, K. Rustan M. Leino, Wolfram Schulte, Herman Venter: The Spec# Programming System: Challenges and Directions. VSTTE 2005: 144-152
38Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLBor-Yuh Evan Chang, K. Rustan M. Leino: Inferring Object Invariants: Extended Abstract. Electr. Notes Theor. Comput. Sci. 131: 63-74 (2005)
37Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Efficient weakest preconditions. Inf. Process. Lett. 93(6): 281-288 (2005)
36Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLLilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, Erik Poll: An overview of JML tools and applications. STTT 7(3): 212-232 (2005)
35Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Todd D. Millstein, James B. Saxe: Generating error traces from verification-condition counterexamples. Sci. Comput. Program. 55(1-3): 209-226 (2005)
2004
34Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Peter Müller: Object Invariants in Dynamic Contexts. ECOOP 2004: 491-516
33Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Challenges in Increasing Tool Support for Programming. ICTAC 2004: 35-35
32Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Wolfram Schulte: Exception Safety for C#. SEFM 2004: 218-227
31Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLViktor Kuncak, K. Rustan M. Leino: On computing the fixpoint of a set of boolean equations CoRR cs.PL/0408045: (2004)
30Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLMichael Burrows, K. Rustan M. Leino: Finding stale-value errors in concurrent programs. Concurrency - Practice and Experience 16(12): 1161-1172 (2004)
29Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLMichael Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte: Verification of Object-Oriented Programs with Invariants. Journal of Object Technology 3(6): 27-56 (2004)
2003
28Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLManuel Fähndrich, K. Rustan M. Leino: Declaring and checking non-null types in an object-oriented language. OOPSLA 2003: 302-312
27Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: A SAT Characterization of Boolean-Program Correctness. SPIN 2003: 104-120
26Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLMartín Abadi, K. Rustan M. Leino: A Logic of Object-Oriented Programs. Verification: Theory and Practice 2003: 11-41
25Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLLilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph Kiniry, Gary T. Leavens, K. Rustan M. Leino, Erik Poll: An overview of JML tools and applications. Electr. Notes Theor. Comput. Sci. 80: 75-91 (2003)
2002
24Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLCormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata: Extended Static Checking for Java. PLDI 2002: 234-245
23Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Arnd Poetzsch-Heffter, Yunhong Zhou: Using Data Groups to Specify and Check Side Effects. PLDI 2002: 246-257
22Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Greg Nelson: Data abstraction and information hiding. ACM Trans. Program. Lang. Syst. 24(5): 491-553 (2002)
2001
21Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLCormac Flanagan, K. Rustan M. Leino: Houdini, an Annotation Assistant for ESC/Java. FME 2001: 500-517
20Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Extended Static Checking: A Ten-Year Perspective. Informatics 2001: 157-175
19Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Applications of Extended Static Checking. SAS 2001: 185-193
18Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Real estate of names. Inf. Process. Lett. 77(2-4): 169-171 (2001)
17Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLCormac Flanagan, Rajeev Joshi, K. Rustan M. Leino: Annotation inference for modular checkers. Inf. Process. Lett. 77(2-4): 97-108 (2001)
2000
16Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLRajeev Joshi, K. Rustan M. Leino: A semantic approach to secure information flow. Sci. Comput. Program. 37(1-3): 113-138 (2000)
1999
15no EE pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, James B. Saxe, Raymie Stata: Checking Java Programs via Guarded Commands. ECOOP Workshops 1999: 110-111
14Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Computing Permutation Encodings. Formal Asp. Comput. 11(1): 56-74 (1999)
13Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Raymie Stata: Virginity: A Contribution to the Specification of Object-Oriented Software. Inf. Process. Lett. 70(2): 99-105 (1999)
12Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Rajit Manohar: Joining Specification Statements. Theor. Comput. Sci. 216(1-2): 375-394 (1999)
1998
11Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Greg Nelson: An Extended Static Checker for Modular-3. CC 1998: 302-305
10Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Recursive Object Types in a Logic of Object-Oriented Programs. ESOP 1998: 170-184
9Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Rajeev Joshi: A Semantic Approach to Secure Information Flow. MPC 1998: 254-271
8Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Data Groups: Specifying the Modification of Extended State. OOPSLA 1998: 144-153
7no EE pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Extended static checking. PROCOMET 1998: 1-2
6no EE pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Recursive Object Types in a Logic of Object-Oriented Programs. Nord. J. Comput. 5(4): 330-360 (1998)
1997
5Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLMartín Abadi, K. Rustan M. Leino: A Logic of Object-Oriented Programs. TAPSOFT 1997: 682-696
1995
4Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: A Method for Showing Progress. Formal Asp. Comput. 7(5): 576-580 (1995)
3Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLRajit Manohar, K. Rustan M. Leino: Conditional Composition. Formal Asp. Comput. 7(6): 683-703 (1995)
2Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino: Constructing a Program with Exceptions. Inf. Process. Lett. 53(3): 159-163 (1995)
1994
1no EE pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLK. Rustan M. Leino, Jan L. A. van de Snepscheut: Semantics of Exceptions. PROCOMET 1994: 447-466

Coauthor Index

1Martín Abadi [5] [26]
2Parosh Aziz Abdulla [82]
3Eyad Alkassar [81]
4Rob Arthan [81]
5Michael Barnett [29] [39] [44] [45] [71]
6Mike Barnett [78]
7Sascha Böhme [59]
8Derek Bronish [81]
9Lilian Burdy [25] [36]
10Michael Burrows [30]
11Bor-Yuh Evan Chang [38] [40] [45]
12Rod Chapman [81]
13Yoonsik Cheon [25] [36]
14Ernie Cohen [81]
15David R. Cok [25] [36]
16Ádám Darvas [53]
17Robert DeLine [29] [39] [45]
18Michael D. Ernst [25] [36]
19Manuel Fähndrich [28] [29] [39] [78]
20Cormac Flanagan [17] [21] [24]
21Claire Le Goues [79]
22Mark A. Hillebrand [81]
23Jochen Hoenicke [66] [69]
24Bart Jacobs [81]
25Bart Jacobs [39] [43] [45] [57]
26Rajeev Joshi [9] [16] [17]
27Joseph Kiniry (Joseph R. Kiniry) [25] [36]
28Vladimir Klebanov [81]
29Viktor Kuncak [31]
30Gary T. Leavens [25] [36] [51] [81]
31Mark Lillibridge [24]
32Francesco Logozzo [48]
33Rajit Manohar [3] [12]
34Ronald Middelkoop [67]
35Todd D. Millstein [35]
36Rosemary Monahan [64] [72] [81]
37Michal Moskal [79]
38Peter Müller [34] [46] [50] [51] [58] [60] [62] [65] [68] [77] [78] [81]
39Madan Musuvathi [41]
40Greg Nelson [11] [22] [24]
41Xinming Ou [41]
42Frank Piessens [43] [57] [81]
43Andreas Podelski [66] [69]
44Arnd Poetzsch-Heffter [23]
45Nadia Polikarpova [81]
46Erik Poll [25] [36]
47Tom Ridge (Thomas Ridge) [81]
48Philipp Rümmer [75]
49James B. Saxe [15] [24] [35]
50Martin Schäf [66] [69]
51Wolfram Schulte [29] [32] [39] [43] [54] [57] [78]
52Natarajan Shankar [81]
53Jan Smans [57] [65] [77] [81]
54Jan L. A. van de Snepscheut [1]
55Raymie Stata [13] [15] [24]
56Stephan Tobies [81]
57Thomas Tuerk [81]
58Mattias Ulbrich [81]
59Herman Venter [39] [78]
60Angela Wallenburg [58] [61]
61Benjamin Weiß [81]
62Thomas Wies [66] [69]
63Burkhart Wolff [59]
64Valentin Wüstholz [81]
65Yunhong Zhou [23]

Colors in the list of coauthors

Home | Conferences | Journals | Series | FAQ — Search: Faceted | Free | Complete | Author
Last update Fri Jun 1 15:44:53 2012 CET by the DBLP Team — This material is Open Data Data released under the ODC-BY 1.0 license — See also our legal information page