| 2009 |
|---|
| 65 | EE | K. Rustan M. Leino,
Peter Müller:
A Basis for Verifying Multi-threaded Programs.
ESOP 2009: 378-393 |
| 64 | EE | K. Rustan M. Leino,
Ronald Middelkoop:
Proving Consistency of Pure Methods and Model Fields.
FASE 2009: 231-245 |
| 63 | EE | K. Rustan M. Leino,
Rosemary Monahan:
Reasoning about comprehensions with first-order SMT solvers.
SAC 2009: 615-622 |
| 2008 |
|---|
| 62 | EE | K. Rustan M. Leino:
Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software Engineering.
COMPSAC 2008: 11 |
| 61 | EE | K. Rustan M. Leino,
Peter Müller:
Verification of Equivalent-Results Methods.
ESOP 2008: 307-321 |
| 60 | EE | K. Rustan M. Leino,
Angela Wallenburg:
Class-local object invariants.
ISEC 2008: 57-66 |
| 59 | EE | Sascha Böhme,
K. Rustan M. Leino,
Burkhart Wolff:
HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier.
TPHOLs 2008: 150-166 |
| 58 | EE | K. Rustan M. Leino,
Peter Müller,
Angela Wallenburg:
Flexible Immutability with Frozen Objects.
VSTTE 2008: 192-208 |
| 57 | EE | Bart 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 |
|---|
| 56 | EE | K. Rustan M. Leino:
Specifying and verifying software.
ASE 2007: 2 |
| 55 | EE | K. Rustan M. Leino:
Designing Verification Conditions for Software.
CADE 2007: 345 |
| 54 | EE | K. Rustan M. Leino,
Wolfram Schulte:
Using History Invariants to Verify Observers.
ESOP 2007: 80-94 |
| 53 | EE | Ádám Darvas,
K. Rustan M. Leino:
Practical Reasoning About Invocations and Implementations of Pure Methods.
FASE 2007: 336-351 |
| 52 | EE | K. Rustan M. Leino:
Verifying Object-Oriented Software: Lessons and Challenges.
TACAS 2007: 2 |
| 51 | EE | Gary 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 |
|---|
| 50 | EE | K. Rustan M. Leino,
Peter Müller:
A Verification Methodology for Model Fields.
ESOP 2006: 115-130 |
| 49 | EE | K. Rustan M. Leino:
Specifying and Verifying Programs in Spec#.
Ershov Memorial Conference 2006: 20 |
| 2005 |
|---|
| 48 | EE | K. Rustan M. Leino,
Francesco Logozzo:
Loop Invariants on Demand.
APLAS 2005: 119-134 |
| 47 | EE | K. Rustan M. Leino:
Program Verification and Programming Methodology.
Abstract State Machines 2005: 73 |
| 46 | EE | K. Rustan M. Leino,
Peter Müller:
Modular Verification of Static Class Invariants.
FM 2005: 26-42 |
| 45 | EE | Michael 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 |
| 44 | EE | Michael Barnett,
K. Rustan M. Leino:
Weakest-precondition of unstructured programs.
PASTE 2005: 82-87 |
| 43 | EE | Bart Jacobs,
Frank Piessens,
K. Rustan M. Leino,
Wolfram Schulte:
Safe Concurrency for Aggregate Objects with Invariants.
SEFM 2005: 137-147 |
| 42 | EE | K. Rustan M. Leino:
Invariants on Demand.
SEFM 2005: 148-149 |
| 41 | EE | K. 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 |
| 40 | EE | Bor-Yuh Evan Chang,
K. Rustan M. Leino:
Abstract Interpretation with Alien Expressions and Heap Structures.
VMCAI 2005: 147-163 |
| 39 | EE | Michael 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 |
| 38 | EE | Bor-Yuh Evan Chang,
K. Rustan M. Leino:
Inferring Object Invariants: Extended Abstract.
Electr. Notes Theor. Comput. Sci. 131: 63-74 (2005) |
| 37 | EE | K. Rustan M. Leino:
Efficient weakest preconditions.
Inf. Process. Lett. 93(6): 281-288 (2005) |
| 36 | EE | Lilian 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) |
| 35 | EE | K. 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 |
|---|
| 34 | EE | K. Rustan M. Leino,
Peter Müller:
Object Invariants in Dynamic Contexts.
ECOOP 2004: 491-516 |
| 33 | EE | K. Rustan M. Leino:
Challenges in Increasing Tool Support for Programming.
ICTAC 2004: 35-35 |
| 32 | EE | K. Rustan M. Leino,
Wolfram Schulte:
Exception Safety for C#.
SEFM 2004: 218-227 |
| 31 | EE | Viktor Kuncak,
K. Rustan M. Leino:
On computing the fixpoint of a set of boolean equations
CoRR cs.PL/0408045: (2004) |
| 30 | EE | Michael Burrows,
K. Rustan M. Leino:
Finding stale-value errors in concurrent programs.
Concurrency - Practice and Experience 16(12): 1161-1172 (2004) |
| 29 | EE | Michael 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 |
|---|
| 28 | EE | Manuel Fähndrich,
K. Rustan M. Leino:
Declaring and checking non-null types in an object-oriented language.
OOPSLA 2003: 302-312 |
| 27 | EE | K. Rustan M. Leino:
A SAT Characterization of Boolean-Program Correctness.
SPIN 2003: 104-120 |
| 26 | EE | Martín Abadi,
K. Rustan M. Leino:
A Logic of Object-Oriented Programs.
Verification: Theory and Practice 2003: 11-41 |
| 25 | EE | Lilian 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: (2003) |
| 2002 |
|---|
| 24 | EE | Cormac Flanagan,
K. Rustan M. Leino,
Mark Lillibridge,
Greg Nelson,
James B. Saxe,
Raymie Stata:
Extended Static Checking for Java.
PLDI 2002: 234-245 |
| 23 | EE | K. Rustan M. Leino,
Arnd Poetzsch-Heffter,
Yunhong Zhou:
Using Data Groups to Specify and Check Side Effects.
PLDI 2002: 246-257 |
| 22 | EE | K. Rustan M. Leino,
Greg Nelson:
Data abstraction and information hiding.
ACM Trans. Program. Lang. Syst. 24(5): 491-553 (2002) |
| 2001 |
|---|
| 21 | EE | Cormac Flanagan,
K. Rustan M. Leino:
Houdini, an Annotation Assistant for ESC/Java.
FME 2001: 500-517 |
| 20 | EE | K. Rustan M. Leino:
Extended Static Checking: A Ten-Year Perspective.
Informatics 2001: 157-175 |
| 19 | EE | K. Rustan M. Leino:
Applications of Extended Static Checking.
SAS 2001: 185-193 |
| 18 | EE | K. Rustan M. Leino:
Real estate of names.
Inf. Process. Lett. 77(2-4): 169-171 (2001) |
| 17 | EE | Cormac Flanagan,
Rajeev Joshi,
K. Rustan M. Leino:
Annotation inference for modular checkers.
Inf. Process. Lett. 77(2-4): 97-108 (2001) |
| 2000 |
|---|
| 16 | | Rajeev Joshi,
K. Rustan M. Leino:
A semantic approach to secure information flow.
Sci. Comput. Program. 37(1-3): 113-138 (2000) |
| 1999 |
|---|
| 15 | | K. Rustan M. Leino,
James B. Saxe,
Raymie Stata:
Checking Java Programs via Guarded Commands.
ECOOP Workshops 1999: 110-111 |
| 14 | EE | K. Rustan M. Leino:
Computing Permutation Encodings.
Formal Asp. Comput. 11(1): 56-74 (1999) |
| 13 | EE | K. Rustan M. Leino,
Raymie Stata:
Virginity: A Contribution to the Specification of Object-Oriented Software.
Inf. Process. Lett. 70(2): 99-105 (1999) |
| 12 | EE | K. Rustan M. Leino,
Rajit Manohar:
Joining Specification Statements.
Theor. Comput. Sci. 216(1-2): 375-394 (1999) |
| 1998 |
|---|
| 11 | | K. Rustan M. Leino,
Greg Nelson:
An Extended Static Checker for Modular-3.
CC 1998: 302-305 |
| 10 | EE | K. Rustan M. Leino:
Recursive Object Types in a Logic of Object-Oriented Programs.
ESOP 1998: 170-184 |
| 9 | EE | K. Rustan M. Leino,
Rajeev Joshi:
A Semantic Approach to Secure Information Flow.
MPC 1998: 254-271 |
| 8 | EE | K. Rustan M. Leino:
Data Groups: Specifying the Modification of Extended State.
OOPSLA 1998: 144-153 |
| 7 | | K. Rustan M. Leino:
Extended static checking.
PROCOMET 1998: 1-2 |
| 6 | | K. Rustan M. Leino:
Recursive Object Types in a Logic of Object-Oriented Programs.
Nord. J. Comput. 5(4): 330-360 (1998) |
| 1997 |
|---|
| 5 | | Martín Abadi,
K. Rustan M. Leino:
A Logic of Object-Oriented Programs.
TAPSOFT 1997: 682-696 |
| 1995 |
|---|
| 4 | | K. Rustan M. Leino:
A Method for Showing Progress.
Formal Asp. Comput. 7(5): 576-580 (1995) |
| 3 | | Rajit Manohar,
K. Rustan M. Leino:
Conditional Composition.
Formal Asp. Comput. 7(6): 683-703 (1995) |
| 2 | EE | K. Rustan M. Leino:
Constructing a Program with Exceptions.
Inf. Process. Lett. 53(3): 159-163 (1995) |
| 1994 |
|---|
| 1 | | K. Rustan M. Leino,
Jan L. A. van de Snepscheut:
Semantics of Exceptions.
PROCOMET 1994: 447-466 |
