K. Rustan M. Leino

131 papers A* 6A 16B 23C 2Misc 2Journal 30Unranked 48
YearRankTypeTitle / Venue / Authors
2026 — conf
A Methodology for Modular Termination Verification.
On the Pursuit of Insight and Elegance
K. Rustan M. Leino
2025 A* conf
Formally Verified Cloud-Scale Authorization.
ICSE
Aleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks, Sam Huang, Georges-Axel Jaloyan, Anjali Joshi, K. Rustan M. Leino, Mikael Mayer, Sean McLaughlin, Akhilesh Mritunjai, Clément Pit-Claudel, Sorawee Porncharoenwase, Florian Rabe, Marianna Rapoport, Giles Reger, Cody Roux, Neha Rungta, Robin Salkeld, Matthias Schlaipfer, Daniel Schoepe, Johanna Schwartzentruber, Serdar Tasiran, Aaron Tomb, Emina Torlak, Jean-Baptiste Tristan, Lucas G. Wagner, Michael W. Whalen, Remy Willems, Tongtong Xiang, Tae Joon Byun, Joshua M. Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, Yongwei Yuan
2025 J jnl
The Design of an Interactive Proof Mode for Dafny.
CoRR
Stefan Ciobâca, K. Rustan M. Leino, Stefan-Alexandru Mercas, Roxana-Mihaela Timon
2024 — conf
Free Facts: An Alternative to Inefficient Axioms in Dafny.
FM (1)
Tabea Bordis, K. Rustan M. Leino
2024 J jnl
Preface of the special issue on the conference on Computer-Aided Verification 2020 and 2021.
Formal Methods Syst. Des.
Aws Albarghouthi, K. Rustan M. Leino, Alexandra Silva, Caterina Urban
2024 B conf
Writing Proofs in Dafny.
FMCAD
K. Rustan M. Leino
2022 — conf
Specifying the Boundary Between Unverified and Verified Code.
The Logic of Software. A Tasting Menu of Formal Methods
David R. Cok, K. Rustan M. Leino
2021 — ed.
Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I
CAV (1)
Alexandra Silva, K. Rustan M. Leino
2021 — ed.
Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II
CAV (2)
Alexandra Silva, K. Rustan M. Leino
2018 — conf
Modular Verification Scopes via Export Sets and Translucent Exports.
Principled Software Development
K. Rustan M. Leino, Daniel Matichuk
2017 J jnl
Accessible Software Verification with Dafny.
IEEE Softw.
K. Rustan M. Leino
2017 — conf
Everest: Towards a Verified, Drop-in Replacement of HTTPS.
SNAPL
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, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean Karim Zinzindohoue
2017 — conf
Modeling Concurrency in Dafny.
SETSS
K. Rustan M. Leino
2017 A* conf
Vale: Verifying High-Performance Cryptographic Assembly Code.
USENIX Security Symposium
Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath T. V. Setty, Laure Thompson
2016 A conf
Integrated Environment for Diagnosing Verification Errors.
TACAS
Maria Christakis, K. Rustan M. Leino, Peter Müller, Valentin Wüstholz
2016 — conf
Quicksort Revisited - Verifying Alternative Versions of Quicksort.
Theory and Practice of Formal Methods
Razvan Certezeanu, Sophia Drossopoulou, Benjamin Egelund-Müller, K. Rustan M. Leino, Sinduran Sivarajan, Mark J. Wheelhouse
2016 — conf
Trigger Selection Strategies to Stabilize Program Verifiers.
CAV (1)
K. Rustan M. Leino, Clément Pit-Claudel
2016 B ed.
Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings
VMCAI
Barbara Jobstmann, K. Rustan M. Leino
2015 J jnl
An Assertional Proof of the Stability and Correctness of Natural Mergesort.
ACM Trans. Comput. Log.
K. Rustan M. Leino, Paqui Lucio
2015 — conf
Automatic verification of Dafny programs with traits.
FTfJP@ECOOP
Reza Ahmadi, K. Rustan M. Leino, Jyrki Nummenmaa
2015 — conf
Compiling Hilbert's epsilon operator.
LPAR (short papers)
K. Rustan M. Leino
2015 — conf
Fine-Grained Caching of Verification Results.
CAV (1)
K. Rustan M. Leino, Valentin Wüstholz
2015 — conf
Programming Language Features for Refinement.
Refine@FM
Jason Koenig, K. Rustan M. Leino
2015 — conf
Well-founded Functions and Extreme Predicates in Dafny: A Tutorial.
IWIL@LPAR
K. Rustan M. Leino
2014 B conf
Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier.
FM
K. Rustan M. Leino, Michal Moskal
2014 — conf
Computing with an SMT Solver.
TAP@STAF
Nada Amin, K. Rustan M. Leino, Tiark Rompf
2014 B conf
Formalizing and Verifying a Modern Build Language.
FM
Maria Christakis, K. Rustan M. Leino, Wolfram Schulte
2014 — conf
The Dafny Integrated Development Environment.
F-IDE
K. Rustan M. Leino, Valentin Wüstholz
2013 B conf
Abstract Read Permissions: Fractional Permissions without the Fractions.
VMCAI
Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers
2013 B conf
Automating Theorem Proving with SMT.
ITP
K. Rustan M. Leino
2013 A* conf
Developing verified programs with dafny.
ICSE
K. Rustan M. Leino
2013 J jnl
PLDI 2002: Extended static checking for Java.
ACM SIGPLAN Notices
Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata
2013 J jnl
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.
Int. J. Softw. Tools Technol. Transf.
Parosh Aziz Abdulla, K. Rustan M. Leino
2013 — conf
Verified Calculations.
VSTTE
K. Rustan M. Leino, Nadia Polikarpova
2012 B conf
Automating Induction with an SMT Solver.
VMCAI
K. Rustan M. Leino
2012 J jnl
Behavioral interface specification languages.
ACM Comput. Surv.
John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew J. Parkinson
2012 — conf
Developing Verified Programs with Dafny.
VSTTE
K. Rustan M. Leino
2012 — conf
Developing verified programs with Dafny.
HILT
K. Rustan M. Leino
2012 — ch.
Getting Started with Dafny: A Guide.
Software Safety and Security
Jason Koenig, K. Rustan M. Leino
2012 A conf
Program extrapolation with jennisys.
OOPSLA
K. Rustan M. Leino, Aleksandar Milicevic
2012 — conf
Program proving using intermediate verification languages (IVLs) like boogie and why3.
HILT
K. Rustan M. Leino
2012 — conf
Staged program development.
SPLASH
K. Rustan M. Leino
2012 J jnl
Stepwise refinement of heap-manipulating code in Chalice.
Formal Aspects Comput.
K. Rustan M. Leino, Kuat Yessenov
2012 — conf
The EventB2Dafny rodin plug-in.
TOPI@ICSE
Néstor Cataño, K. Rustan M. Leino, Víctor Rivera
2011 — conf
Fractional permissions without the fractions.
FTfJP@ECOOP
Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers
2011 — conf
From Retrospective Verification to Forward-Looking Development.
NASA Formal Methods
K. Rustan M. Leino
2011 J jnl
Specification and verification: the Spec# experience.
Commun. ACM
Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, Herman Venter
2011 B conf
The 1st Verified Software Competition: Experience Report.
FM
Vladimir 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ß
2011 B conf
The Boogie Verification Debugger (Tool Paper).
SEFM
Claire Le Goues, K. Rustan M. Leino, Michal Moskal
2011 A ed.
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
TACAS
Parosh Aziz Abdulla, K. Rustan M. Leino
2011 — conf
Using Dafny, an Automatic Program Verifier.
LASER Summer School
Luke Herbert, K. Rustan M. Leino, Jose Quaresma
2010 A conf
A Polymorphic Intermediate Verification Language: Design and Logical Encoding.
TACAS
K. Rustan M. Leino, Philipp Rümmer
2010 — conf
Dafny Meets the Verification Benchmarks Challenge.
VSTTE
K. Rustan M. Leino, Rosemary Monahan
2010 — conf
Dafny: An Automatic Program Verifier for Functional Correctness.
LPAR (Dakar)
K. Rustan M. Leino
2010 A conf
Deadlock-Free Channels and Locks.
ESOP
K. Rustan M. Leino, Peter Müller, Jan Smans
2010 J jnl
Doomed program points.
Formal Methods Syst. Des.
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies
2010 J jnl
Learning to do program verification.
Commun. ACM
K. Rustan M. Leino
2010 — conf
To Goto Where No Statement Has Gone Before.
VSTTE
Michael Barnett, K. Rustan M. Leino
2010 — conf
Tools and Behavioral Abstraction: A Direction for Software Engineering.
The Future of Software Engineering
K. Rustan M. Leino
2010 B conf
Verifying Concurrent Programs with Chalice.
VMCAI
K. Rustan M. Leino
2009 A conf
A Basis for Verifying Multi-threaded Programs.
ESOP
K. Rustan M. Leino, Peter Müller
2009 B conf
It's Doomed; We Can Prove It.
FM
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies
2009 B conf
Proving Consistency of Pure Methods and Model Fields.
FASE
K. Rustan M. Leino, Ronald Middelkoop
2009 Misc conf
Reasoning about comprehensions with first-order SMT solvers.
SAC
K. Rustan M. Leino, Rosemary Monahan
2009 — conf
Verification of Concurrent Programs with Chalice.
FOSAD
K. Rustan M. Leino, Peter Müller, Jan Smans
2008 J jnl
A programming model for concurrent object-oriented programs.
ACM Trans. Program. Lang. Syst.
Bart Jacobs, Frank Piessens, Jan Smans, K. Rustan M. Leino, Wolfram Schulte
2008 — conf
Class-local object invariants.
ISEC
K. Rustan M. Leino, Angela Wallenburg
2008 — conf
Flexible Immutability with Frozen Objects.
VSTTE
K. Rustan M. Leino, Peter Müller, Angela Wallenburg
2008 — conf
HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier.
TPHOLs
Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff
2008 B conf
Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software Engineering.
COMPSAC
K. Rustan M. Leino
2008 — conf
Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs.
LASER Summer School
K. Rustan M. Leino, Peter Müller
2008 A conf
Verification of Equivalent-Results Methods.
ESOP
K. Rustan M. Leino, Peter Müller
2007 A conf
Designing Verification Conditions for Software.
CADE
K. Rustan M. Leino
2007 B conf
Practical Reasoning About Invocations and Implementations of Pure Methods.
FASE
Ádám Darvas, K. Rustan M. Leino
2007 J jnl
Specification and verification challenges for sequential object-oriented programs.
Formal Aspects Comput.
Gary T. Leavens, K. Rustan M. Leino, Peter Müller
2007 A* conf
Specifying and verifying software.
ASE
K. Rustan M. Leino
2007 A conf
Using History Invariants to Verify Observers.
ESOP
K. Rustan M. Leino, Wolfram Schulte
2007 A conf
Verifying Object-Oriented Software: Lessons and Challenges.
TACAS
K. Rustan M. Leino
2006 A conf
A Verification Methodology for Model Fields.
ESOP
K. Rustan M. Leino, Peter Müller
2006 — conf
Specifying and Verifying Programs in Spec#.
Ershov Memorial Conference
K. Rustan M. Leino
2005 A conf
A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover.
TACAS
K. Rustan M. Leino, Madan Musuvathi, Xinming Ou
2005 B conf
Abstract Interpretation with Alien Expressions and Heap Structures.
VMCAI
Bor-Yuh Evan Chang, K. Rustan M. Leino
2005 J jnl
An overview of JML tools and applications.
Int. J. Softw. Tools Technol. Transf.
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, Erik Poll
2005 — conf
Boogie: A Modular Reusable Verifier for Object-Oriented Programs.
FMCO
Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, K. Rustan M. Leino
2005 J jnl
Efficient weakest preconditions.
Inf. Process. Lett.
K. Rustan M. Leino
2005 J jnl
Generating error traces from verification-condition counterexamples.
Sci. Comput. Program.
K. Rustan M. Leino, Todd D. Millstein, James B. Saxe
2005 — conf
Inferring Object Invariants: Extended Abstract.
AIOOL@VMCAI
Bor-Yuh Evan Chang, K. Rustan M. Leino
2005 B conf
Invariants on Demand.
SEFM
K. Rustan M. Leino
2005 B conf
Loop Invariants on Demand.
APLAS
K. Rustan M. Leino, Francesco Logozzo
2005 B conf
Modular Verification of Static Class Invariants.
FM
K. Rustan M. Leino, Peter Müller
2005 — conf
Program Verification and Programming Methodology.
Abstract State Machines
K. Rustan M. Leino
2005 B conf
Safe Concurrency for Aggregate Objects with Invariants.
SEFM
Bart Jacobs, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte
2005 — conf
The Spec# Programming System: Challenges and Directions.
VSTTE
Michael Barnett, Robert DeLine, Manuel Fähndrich, Bart Jacobs, K. Rustan M. Leino, Wolfram Schulte, Herman Venter
2005 — conf
Weakest-precondition of unstructured programs.
PASTE
Michael Barnett, K. Rustan M. Leino
2004 C conf
Challenges in Increasing Tool Support for Programming.
ICTAC
K. Rustan M. Leino
2004 B conf
Exception Safety for C#.
SEFM
K. Rustan M. Leino, Wolfram Schulte
2004 J jnl
Finding stale-value errors in concurrent programs.
Concurr. Pract. Exp.
Michael Burrows, K. Rustan M. Leino
2004 A conf
Object Invariants in Dynamic Contexts.
ECOOP
K. Rustan M. Leino, Peter Müller
2004 J jnl
On computing the fixpoint of a set of boolean equations
CoRR
Viktor Kuncak, K. Rustan M. Leino
2004 — conf
The Spec# Programming System: An Overview.
CASSIS
Mike Barnett, K. Rustan M. Leino, Wolfram Schulte
2004 J jnl
Verification of Object-Oriented Programs with Invariants.
J. Object Technol.
Michael Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte
2003 — conf
A Logic of Object-Oriented Programs.
Verification: Theory and Practice
Martín Abadi, K. Rustan M. Leino
2003 — conf
A SAT Characterization of Boolean-Program Correctness.
SPIN
K. Rustan M. Leino
2003 C conf
An overview of JML tools and applications.
FMICS
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph Kiniry, Gary T. Leavens, K. Rustan M. Leino, Erik Poll
2003 A conf
Declaring and checking non-null types in an object-oriented language.
OOPSLA
Manuel Fähndrich, K. Rustan M. Leino
2002 J jnl
Data abstraction and information hiding.
ACM Trans. Program. Lang. Syst.
K. Rustan M. Leino, Greg Nelson
2002 A* conf
Extended Static Checking for Java.
PLDI
Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata
2002 A* conf
Using Data Groups to Specify and Check Side Effects.
PLDI
K. Rustan M. Leino, Arnd Poetzsch-Heffter, Yunhong Zhou
2001 J jnl
Annotation inference for modular checkers.
Inf. Process. Lett.
Cormac Flanagan, Rajeev Joshi, K. Rustan M. Leino
2001 B conf
Applications of Extended Static Checking.
SAS
K. Rustan M. Leino
2001 Misc conf
Extended Static Checking: A Ten-Year Perspective.
Informatics
K. Rustan M. Leino
2001 — conf
Houdini, an Annotation Assistant for ESC/Java.
FME
Cormac Flanagan, K. Rustan M. Leino
2001 J jnl
Real estate of names.
Inf. Process. Lett.
K. Rustan M. Leino
2000 J jnl
A semantic approach to secure information flow.
Sci. Comput. Program.
Rajeev Joshi, K. Rustan M. Leino
2000 — conf
JML (poster session): notations and tools supporting detailed design in Java.
OOPSLA Addendum
Gary T. Leavens, Clyde Ruby, K. Rustan M. Leino, Erik Poll, Bart Jacobs
1999 — conf
Checking Java Programs via Guarded Commands.
ECOOP Workshops
K. Rustan M. Leino, James B. Saxe, Raymie Stata
1999 J jnl
Computing Permutation Encodings.
Formal Aspects Comput.
K. Rustan M. Leino
1999 J jnl
Joining Specification Statements.
Theor. Comput. Sci.
K. Rustan M. Leino, Rajit Manohar
1999 J jnl
Virginity: A Contribution to the Specification of Object-Oriented Software.
Inf. Process. Lett.
K. Rustan M. Leino, Raymie Stata
1998 B conf
A Semantic Approach to Secure Information Flow.
MPC
K. Rustan M. Leino, Rajeev Joshi
1998 B conf
An Extended Static Checker for Modular-3.
CC
K. Rustan M. Leino, Greg Nelson
1998 A conf
Data Groups: Specifying the Modification of Extended State.
OOPSLA
K. Rustan M. Leino
1998 — conf
Extended static checking.
PROCOMET
K. Rustan M. Leino
1998 A conf
Recursive Object Types in a Logic of Object-Oriented Programs.
ESOP
K. Rustan M. Leino
1998 J jnl
Recursive Object Types in a Logic of Object-Oriented Programs.
Nord. J. Comput.
K. Rustan M. Leino
1997 — conf
A Logic of Object-Oriented Programs.
TAPSOFT
Martín Abadi, K. Rustan M. Leino
1995 J jnl
A Method for Showing Progress.
Formal Aspects Comput.
K. Rustan M. Leino
1995 J jnl
Conditional Composition.
Formal Aspects Comput.
Rajit Manohar, K. Rustan M. Leino
1995 J jnl
Constructing a Program with Exceptions.
Inf. Process. Lett.
K. Rustan M. Leino
1995 — —
Toward reliable modular programs.
K. Rustan M. Leino
1994 — conf
Semantics of Exceptions.
PROCOMET
K. Rustan M. Leino, Jan L. A. van de Snepscheut