Semantics of Exceptions. - K. Rustan M. Leino; Jan L. A. van de Snepscheut (PROCOMET, 1994)

A Method for Showing Progress. - K. Rustan M. Leino (Formal Aspects Comput., 1995)

Conditional Composition. - Rajit Manohar; K. Rustan M. Leino (Formal Aspects Comput., 1995)

Constructing a Program with Exceptions. - K. Rustan M. Leino (Inf. Process. Lett., 1995)

Toward reliable modular programs. - K. Rustan M. Leino (1995)

An Extended Static Checker for Modular-3. - K. Rustan M. Leino; Greg Nelson (CC, 1998)

Data Groups: Specifying the Modification of Extended State. - K. Rustan M. Leino (OOPSLA, 1998)

Extended static checking. - K. Rustan M. Leino (PROCOMET, 1998)

Recursive Object Types in a Logic of Object-Oriented Programs. - K. Rustan M. Leino (Nord. J. Comput., 1998)

Checking Java Programs via Guarded Commands. - K. Rustan M. Leino; James B. Saxe; Raymie Stata (ECOOP Workshops, 1999)

Computing Permutation Encodings. - K. Rustan M. Leino (Formal Aspects Comput., 1999)

Virginity: A Contribution to the Specification of Object-Oriented Software. - K. Rustan M. Leino; Raymie Stata (Inf. Process. Lett., 1999)

Joining Specification Statements. - K. Rustan M. Leino; Rajit Manohar (Theor. Comput. Sci., 1999)

JML (poster session): notations and tools supporting detailed design in Java. - Gary T. Leavens; Clyde Ruby; K. Rustan M. Leino; Erik Poll; Bart Jacobs 001 (OOPSLA Addendum, 2000)

A semantic approach to secure information flow. - Rajeev Joshi; K. Rustan M. Leino (Sci. Comput. Program., 2000)

Extended Static Checking: A Ten-Year Perspective. - K. Rustan M. Leino (Informatics, 2001)

Houdini, an Annotation Assistant for ESC/Java. - Cormac Flanagan; K. Rustan M. Leino (FME, 2001)

Applications of Extended Static Checking. - K. Rustan M. Leino (SAS, 2001)

Annotation inference for modular checkers. - Cormac Flanagan; Rajeev Joshi; K. Rustan M. Leino (Inf. Process. Lett., 2001)

Real estate of names. - K. Rustan M. Leino (Inf. Process. Lett., 2001)

Extended Static Checking for Java. - Cormac Flanagan; K. Rustan M. Leino; Mark Lillibridge; Greg Nelson; James B. Saxe; Raymie Stata (PLDI, 2002)

Using Data Groups to Specify and Check Side Effects. - K. Rustan M. Leino; Arnd Poetzsch-Heffter; Yunhong Zhou (PLDI, 2002)

Data abstraction and information hiding. - K. Rustan M. Leino; Greg Nelson (ACM Trans. Program. Lang. Syst., 2002)

A Logic of Object-Oriented Programs. - Martín Abadi; K. Rustan M. Leino (Verification: Theory and Practice, 2003)

Declaring and checking non-null types in an object-oriented language. - Manuel Fähndrich; K. Rustan M. Leino (OOPSLA, 2003)

A SAT Characterization of Boolean-Program Correctness. - K. Rustan M. Leino (SPIN, 2003)

The Spec# Programming System: An Overview. - Mike Barnett 001; K. Rustan M. Leino; Wolfram Schulte (CASSIS, 2004)

Object Invariants in Dynamic Contexts. - K. Rustan M. Leino; Peter Müller 001 (ECOOP, 2004)

Challenges in Increasing Tool Support for Programming. - K. Rustan M. Leino (ICTAC, 2004)

Exception Safety for C#. - K. Rustan M. Leino; Wolfram Schulte (SEFM, 2004)

Finding stale-value errors in concurrent programs. - Michael Burrows; K. Rustan M. Leino (Concurr. Pract. Exp., 2004)

On computing the fixpoint of a set of boolean equations - Viktor Kuncak; K. Rustan M. Leino (CoRR, 2004)

Verification of Object-Oriented Programs with Invariants. - Michael Barnett 001; Robert DeLine; Manuel Fähndrich; K. Rustan M. Leino; Wolfram Schulte (J. Object Technol., 2004)

Loop Invariants on Demand. - K. Rustan M. Leino; Francesco Logozzo (APLAS, 2005)

Program Verification and Programming Methodology. - K. Rustan M. Leino (Abstract State Machines, 2005)

Modular Verification of Static Class Invariants. - K. Rustan M. Leino; Peter Müller 001 (FM, 2005)

Boogie: A Modular Reusable Verifier for Object-Oriented Programs. - Michael Barnett 001; Bor-Yuh Evan Chang; Robert DeLine; Bart Jacobs 002; K. Rustan M. Leino (FMCO, 2005)

Weakest-precondition of unstructured programs. - Michael Barnett 001; K. Rustan M. Leino (PASTE, 2005)

Safe Concurrency for Aggregate Objects with Invariants. - Bart Jacobs 002; Frank Piessens; K. Rustan M. Leino; Wolfram Schulte (SEFM, 2005)

Invariants on Demand. - K. Rustan M. Leino (SEFM, 2005)

A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover. - K. Rustan M. Leino; Madan Musuvathi; Xinming Ou (TACAS, 2005)

Abstract Interpretation with Alien Expressions and Heap Structures. - Bor-Yuh Evan Chang; K. Rustan M. Leino (VMCAI, 2005)

The Spec# Programming System: Challenges and Directions. - Michael Barnett 001; Robert DeLine; Manuel Fähndrich; Bart Jacobs 002; K. Rustan M. Leino; Wolfram Schulte; Herman Venter (VSTTE, 2005)

Inferring Object Invariants: Extended Abstract. - Bor-Yuh Evan Chang; K. Rustan M. Leino (AIOOL@VMCAI, 2005)

Efficient weakest preconditions. - K. Rustan M. Leino (Inf. Process. Lett., 2005)

Generating error traces from verification-condition counterexamples. - K. Rustan M. Leino; Todd D. Millstein; James B. Saxe (Sci. Comput. Program., 2005)

An overview of JML tools and applications. - Lilian Burdy; Yoonsik Cheon; David R. Cok; Michael D. Ernst; Joseph R. Kiniry; Gary T. Leavens; K. Rustan M. Leino; Erik Poll (Int. J. Softw. Tools Technol. Transf., 2005)

Specifying and Verifying Programs in Spec#. - K. Rustan M. Leino (Ershov Memorial Conference, 2006)

A Verification Methodology for Model Fields. - K. Rustan M. Leino; Peter Müller 001 (ESOP, 2006)

Designing Verification Conditions for Software. - K. Rustan M. Leino (CADE, 2007)

Using History Invariants to Verify Observers. - K. Rustan M. Leino; Wolfram Schulte (ESOP, 2007)

Practical Reasoning About Invocations and Implementations of Pure Methods. - Ádám Darvas; K. Rustan M. Leino (FASE, 2007)

Specifying and verifying software. - K. Rustan M. Leino (ASE, 2007)

Verifying Object-Oriented Software: Lessons and Challenges. - K. Rustan M. Leino (TACAS, 2007)

Specification and verification challenges for sequential object-oriented programs. - Gary T. Leavens; K. Rustan M. Leino; Peter Müller 001 (Formal Aspects Comput., 2007)

Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software Engineering. - K. Rustan M. Leino (COMPSAC, 2008)

Verification of Equivalent-Results Methods. - K. Rustan M. Leino; Peter Müller 001 (ESOP, 2008)

Class-local object invariants. - K. Rustan M. Leino; Angela Wallenburg (ISEC, 2008)

Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs. - K. Rustan M. Leino; Peter Müller 001 (LASER Summer School, 2008)

HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier. - Sascha Böhme; K. Rustan M. Leino; Burkhart Wolff (TPHOLs, 2008)

Flexible Immutability with Frozen Objects. - K. Rustan M. Leino; Peter Müller 001; Angela Wallenburg (VSTTE, 2008)

A programming model for concurrent object-oriented programs. - Bart Jacobs 002; Frank Piessens; Jan Smans; K. Rustan M. Leino; Wolfram Schulte (ACM Trans. Program. Lang. Syst., 2008)

A Basis for Verifying Multi-threaded Programs. - K. Rustan M. Leino; Peter Müller 001 (ESOP, 2009)

Proving Consistency of Pure Methods and Model Fields. - K. Rustan M. Leino; Ronald Middelkoop (FASE, 2009)

It's Doomed; We Can Prove It. - Jochen Hoenicke; K. Rustan M. Leino; Andreas Podelski; Martin Schäf; Thomas Wies (FM, 2009)

Verification of Concurrent Programs with Chalice. - K. Rustan M. Leino; Peter Müller 001; Jan Smans (FOSAD, 2009)

Reasoning about comprehensions with first-order SMT solvers. - K. Rustan M. Leino; Rosemary Monahan (SAC, 2009)

Tools and Behavioral Abstraction: A Direction for Software Engineering. - K. Rustan M. Leino (The Future of Software Engineering, 2010)

Deadlock-Free Channels and Locks. - K. Rustan M. Leino; Peter Müller 001; Jan Smans (ESOP, 2010)

Dafny: An Automatic Program Verifier for Functional Correctness. - K. Rustan M. Leino (LPAR (Dakar), 2010)

A Polymorphic Intermediate Verification Language: Design and Logical Encoding. - K. Rustan M. Leino; Philipp Rümmer (TACAS, 2010)

Verifying Concurrent Programs with Chalice. - K. Rustan M. Leino (VMCAI, 2010)

To Goto Where No Statement Has Gone Before. - Michael Barnett 001; K. Rustan M. Leino (VSTTE, 2010)

Dafny Meets the Verification Benchmarks Challenge. - K. Rustan M. Leino; Rosemary Monahan (VSTTE, 2010)

Learning to do program verification. - K. Rustan M. Leino (Commun. ACM, 2010)

Doomed program points. - Jochen Hoenicke; K. Rustan M. Leino; Andreas Podelski; Martin Schäf; Thomas Wies (Formal Methods Syst. Des., 2010)

Fractional permissions without the fractions. - Stefan Heule; K. Rustan M. Leino; Peter Müller 001; Alexander J. Summers (FTfJP@ECOOP, 2011)

The 1st Verified Software Competition: Experience Report. - Vladimir Klebanov; Peter Müller 001; Natarajan Shankar; Gary T. Leavens; Valentin Wüstholz; Eyad Alkassar; Rob Arthan; Derek Bronish; Rod Chapman; Ernie Cohen; Mark A. Hillebrand; Bart Jacobs 002; et al. (FM, 2011)

Using Dafny, an Automatic Program Verifier. - Luke Herbert; K. Rustan M. Leino; Jose Quaresma (LASER Summer School, 2011)

From Retrospective Verification to Forward-Looking Development. - K. Rustan M. Leino (NASA Formal Methods, 2011)

The Boogie Verification Debugger (Tool Paper). - Claire Le Goues; K. Rustan M. Leino; Michal Moskal (SEFM, 2011)

Specification and verification: the Spec# experience. - Mike Barnett 001; Manuel Fähndrich; K. Rustan M. Leino; Peter Müller 001; Wolfram Schulte; Herman Venter (Commun. ACM, 2011)

The EventB2Dafny rodin plug-in. - Néstor Cataño; K. Rustan M. Leino; Víctor Rivera (TOPI@ICSE, 2012)

Staged program development. - K. Rustan M. Leino (SPLASH, 2012)

Program extrapolation with jennisys. - K. Rustan M. Leino; Aleksandar Milicevic (OOPSLA, 2012)

Program proving using intermediate verification languages (IVLs) like boogie and why3. - K. Rustan M. Leino (HILT, 2012)

Automating Induction with an SMT Solver. - K. Rustan M. Leino (VMCAI, 2012)

Developing Verified Programs with Dafny. - K. Rustan M. Leino (VSTTE, 2012)

Behavioral interface specification languages. - John Hatcliff; Gary T. Leavens; K. Rustan M. Leino; Peter Müller 001; Matthew J. Parkinson (ACM Comput. Surv., 2012)

Stepwise refinement of heap-manipulating code in Chalice. - K. Rustan M. Leino; Kuat Yessenov (Formal Aspects Comput., 2012)

Getting Started with Dafny: A Guide. - Jason Koenig; K. Rustan M. Leino (Software Safety and Security, 2012)

Automating Theorem Proving with SMT. - K. Rustan M. Leino (ITP, 2013)

Abstract Read Permissions: Fractional Permissions without the Fractions. - Stefan Heule; K. Rustan M. Leino; Peter Müller 001; Alexander J. Summers (VMCAI, 2013)

Verified Calculations. - K. Rustan M. Leino; Nadia Polikarpova (VSTTE, 2013)

PLDI 2002: Extended static checking for Java. - Cormac Flanagan; K. Rustan M. Leino; Mark Lillibridge; Greg Nelson; James B. Saxe; Raymie Stata (ACM SIGPLAN Notices, 2013)

Tools for software verification - Introduction to the special section from the seventeenth international conference on tools and algorithms for the construction and analysis of systems. - Parosh Aziz Abdulla; K. Rustan M. Leino (Int. J. Softw. Tools Technol. Transf., 2013)

Formalizing and Verifying a Modern Build Language. - Maria Christakis; K. Rustan M. Leino; Wolfram Schulte (FM, 2014)

Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier. - K. Rustan M. Leino; Michal Moskal (FM, 2014)

Computing with an SMT Solver. - Nada Amin; K. Rustan M. Leino; Tiark Rompf (TAP@STAF, 2014)

The Dafny Integrated Development Environment. - K. Rustan M. Leino; Valentin Wüstholz (F-IDE, 2014)

Fine-Grained Caching of Verification Results. - K. Rustan M. Leino; Valentin Wüstholz (CAV (1), 2015)

Automatic verification of Dafny programs with traits. - Reza Ahmadi; K. Rustan M. Leino; Jyrki Nummenmaa (FTfJP@ECOOP, 2015)

Compiling Hilbert's epsilon operator. - K. Rustan M. Leino (LPAR (short papers), 2015)

Well-founded Functions and Extreme Predicates in Dafny: A Tutorial. - K. Rustan M. Leino (IWIL@LPAR, 2015)

Programming Language Features for Refinement. - Jason Koenig; K. Rustan M. Leino (Refine@FM, 2015)

An Assertional Proof of the Stability and Correctness of Natural Mergesort. - K. Rustan M. Leino; Paqui Lucio (ACM Trans. Comput. Log., 2015)

Quicksort Revisited - Verifying Alternative Versions of Quicksort. - Razvan Certezeanu; Sophia Drossopoulou; Benjamin Egelund-Müller; K. Rustan M. Leino; Sinduran Sivarajan; Mark J. Wheelhouse (Theory and Practice of Formal Methods, 2016)

Trigger Selection Strategies to Stabilize Program Verifiers. - K. Rustan M. Leino; Clément Pit-Claudel (CAV (1), 2016)

Integrated Environment for Diagnosing Verification Errors. - Maria Christakis; K. Rustan M. Leino; Peter Müller 001; Valentin Wüstholz (TACAS, 2016)

Modeling Concurrency in Dafny. - K. Rustan M. Leino (SETSS, 2017)

Everest: Towards a Verified, Drop-in Replacement of HTTPS. - Karthikeyan Bhargavan; Barry Bond; Antoine Delignat-Lavaud; Cédric Fournet; Chris Hawblitzel; Catalin Hritcu; Samin Ishtiaq; Markulf Kohlweiss; K. Rustan M. Leino; Jay R. Lorch; Kenji Maillard; Jianyang Pan; et al. (SNAPL, 2017)

Vale: Verifying High-Performance Cryptographic Assembly Code. - Barry Bond; Chris Hawblitzel; Manos Kapritsos; K. Rustan M. Leino; Jacob R. Lorch; Bryan Parno; Ashay Rane; Srinath T. V. Setty; Laure Thompson (USENIX Security Symposium, 2017)

Accessible Software Verification with Dafny. - K. Rustan M. Leino (IEEE Softw., 2017)

Modular Verification Scopes via Export Sets and Translucent Exports. - K. Rustan M. Leino; Daniel Matichuk (Principled Software Development, 2018)

Specifying the Boundary Between Unverified and Verified Code. - David R. Cok; K. Rustan M. Leino (The Logic of Software. A Tasting Menu of Formal Methods, 2022)

Free Facts: An Alternative to Inefficient Axioms in Dafny. - Tabea Bordis; K. Rustan M. Leino (FM (1), 2024)

Writing Proofs in Dafny. - K. Rustan M. Leino (FMCAD, 2024)

Preface of the special issue on the conference on Computer-Aided Verification 2020 and 2021. - Aws Albarghouthi; K. Rustan M. Leino; Alexandra Silva 001; Caterina Urban (Formal Methods Syst. Des., 2024)

Formally Verified Cloud-Scale Authorization. - Aleks Chakarov; Jaco Geldenhuys; Matthew Heck; Michael Hicks 001; Sam Huang; Georges-Axel Jaloyan; Anjali Joshi; K. Rustan M. Leino; Mikael Mayer; Sean McLaughlin; Akhilesh Mritunjai; Clément Pit-Claudel; et al. (ICSE, 2025)