K. Rustan M. Leino

According to our database, K. Rustan M. Leino authored at least 117 papers between 1994 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2024

Preface of the special issue on the conference on Computer-Aided Verification 2020 and 2021.

Aws Albarghouthi, K. Rustan M. Leino, Alexandra Silva, Caterina Urban

Formal Methods Syst. Des., October, 2024

Free Facts: An Alternative to Inefficient Axioms in Dafny.

Tabea Bordis, K. Rustan M. Leino

Proceedings of the Formal Methods - 26th International Symposium, 2024

2022

Specifying the Boundary Between Unverified and Verified Code.

David R. Cok, K. Rustan M. Leino

Proceedings of the Logic of Software. A Tasting Menu of Formal Methods, 2022

2018

Modular Verification Scopes via Export Sets and Translucent Exports.

K. Rustan M. Leino, Daniel Matichuk

Proceedings of the Principled Software Development, 2018

2017

Accessible Software Verification with Dafny.

K. Rustan M. Leino

IEEE Softw., 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

Proceedings of the 26th USENIX Security Symposium, 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, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella Béguelin, Jean Karim Zinzindohoue

Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

Modeling Concurrency in Dafny.

K. Rustan M. Leino

Proceedings of the Engineering Trustworthy Software Systems - Third International School, 2017

2016

Integrated Environment for Diagnosing Verification Errors.

Maria Christakis, K. Rustan M. Leino, Peter Müller, Valentin Wüstholz

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Trigger Selection Strategies to Stabilize Program Verifiers.

K. Rustan M. Leino, Clément Pit-Claudel

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Quicksort Revisited - Verifying Alternative Versions of Quicksort.

Razvan Certezeanu, Sophia Drossopoulou, Benjamin Egelund-Müller, K. Rustan M. Leino, Sinduran Sivarajan, Mark J. Wheelhouse

Proceedings of the Theory and Practice of Formal Methods, 2016

2015

An Assertional Proof of the Stability and Correctness of Natural Mergesort.

K. Rustan M. Leino, Paqui Lucio

ACM Trans. Comput. Log., 2015

Programming Language Features for Refinement.

Jason Koenig, K. Rustan M. Leino

Proceedings of the Proceedings 17th International Workshop on Refinement, 2015

Well-founded Functions and Extreme Predicates in Dafny: A Tutorial.

K. Rustan M. Leino

Proceedings of the IWIL@LPAR 2015, 2015

Compiling Hilbert's epsilon operator.

K. Rustan M. Leino

Proceedings of the 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, 2015

Automatic verification of Dafny programs with traits.

Reza Ahmadi, K. Rustan M. Leino, Jyrki Nummenmaa

Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, 2015

Fine-Grained Caching of Verification Results.

K. Rustan M. Leino, Valentin Wüstholz

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

The Dafny Integrated Development Environment.

K. Rustan M. Leino, Valentin Wüstholz

Proceedings of the Proceedings 1st Workshop on Formal Integrated Development Environment, 2014

Computing with an SMT Solver.

Nada Amin, K. Rustan M. Leino, Tiark Rompf

Proceedings of the Tests and Proofs - 8th International Conference, 2014

Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier.

K. Rustan M. Leino, Michal Moskal

Proceedings of the FM 2014: Formal Methods, 2014

Formalizing and Verifying a Modern Build Language.

Maria Christakis, K. Rustan M. Leino, Wolfram Schulte

Proceedings of the FM 2014: Formal Methods, 2014

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

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

Verified Calculations.

K. Rustan M. Leino, Nadia Polikarpova

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Abstract Read Permissions: Fractional Permissions without the Fractions.

Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers

Proceedings of the Verification, 2013

Automating Theorem Proving with SMT.

K. Rustan M. Leino

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

Getting Started with Dafny: A Guide.

Jason Koenig, K. Rustan M. Leino

Proceedings of the Software Safety and Security - Tools for Analysis and Verification, 2012

Stepwise refinement of heap-manipulating code in Chalice.

K. Rustan M. Leino, Kuat Yessenov

Formal Aspects Comput., 2012

Behavioral interface specification languages.

John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew J. Parkinson

ACM Comput. Surv., 2012

Developing Verified Programs with Dafny.

K. Rustan M. Leino

Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

Automating Induction with an SMT Solver.

K. Rustan M. Leino

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

Program proving using intermediate verification languages (IVLs) like boogie and why3.

K. Rustan M. Leino

Proceedings of the 2012 ACM Conference on High Integrity Language Technology, 2012

Program extrapolation with jennisys.

K. Rustan M. Leino, Aleksandar Milicevic

Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

Staged program development.

K. Rustan M. Leino

Proceedings of the SPLASH'12, 2012

The EventB2Dafny rodin plug-in.

Néstor Cataño, K. Rustan M. Leino, Víctor Rivera

Proceedings of the Second International Workshop on Developing Tools as Plug-Ins, 2012

2011

Specification and verification: the Spec# experience.

Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, Herman Venter

Commun. ACM, 2011

The Boogie Verification Debugger (Tool Paper).

Claire Le Goues, K. Rustan M. Leino, Michal Moskal

Proceedings of the Software Engineering and Formal Methods - 9th International Conference, 2011

From Retrospective Verification to Forward-Looking Development.

K. Rustan M. Leino

Proceedings of the NASA Formal Methods, 2011

Using Dafny, an Automatic Program Verifier.

Luke Herbert, K. Rustan M. Leino, Jose Quaresma

Proceedings of the Tools for Practical Software Verification, 2011

The 1st Verified Software Competition: Experience Report.

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ß

Proceedings of the FM 2011: Formal Methods, 2011

Fractional permissions without the fractions.

Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers

Proceedings of the 13th Workshop on Formal Techniques for Java-Like Programs, 2011

2010

Doomed program points.

Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies

Formal Methods Syst. Des., 2010

Learning to do program verification.

K. Rustan M. Leino

Commun. ACM, 2010

Dafny Meets the Verification Benchmarks Challenge.

K. Rustan M. Leino, Rosemary Monahan

Proceedings of the Verified Software: Theories, 2010

To Goto Where No Statement Has Gone Before.

Michael Barnett, K. Rustan M. Leino

Proceedings of the Verified Software: Theories, 2010

Verifying Concurrent Programs with Chalice.

K. Rustan M. Leino

Proceedings of the Verification, 2010

A Polymorphic Intermediate Verification Language: Design and Logical Encoding.

K. Rustan M. Leino, Philipp Rümmer

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Dafny: An Automatic Program Verifier for Functional Correctness.

K. Rustan M. Leino

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Deadlock-Free Channels and Locks.

K. Rustan M. Leino, Peter Müller, Jan Smans

Proceedings of the Programming Languages and Systems, 2010

Tools and Behavioral Abstraction: A Direction for Software Engineering.

K. Rustan M. Leino

Proceedings of the Future of Software Engineering., 2010

2009

Reasoning about comprehensions with first-order SMT solvers.

K. Rustan M. Leino, Rosemary Monahan

Proceedings of the 2009 ACM Symposium on Applied Computing (SAC), 2009

Verification of Concurrent Programs with Chalice.

K. Rustan M. Leino, Peter Müller, Jan Smans

Proceedings of the Foundations of Security Analysis and Design V, 2009

It's Doomed; We Can Prove It.

Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies

Proceedings of the FM 2009: Formal Methods, 2009

Proving Consistency of Pure Methods and Model Fields.

K. Rustan M. Leino, Ronald Middelkoop

Proceedings of the Fundamental Approaches to Software Engineering, 2009

A Basis for Verifying Multi-threaded Programs.

K. Rustan M. Leino, Peter Müller

Proceedings of the Programming Languages and Systems, 2009

2008

A programming model for concurrent object-oriented programs.

Bart Jacobs, Frank Piessens, Jan Smans, K. Rustan M. Leino, Wolfram Schulte

ACM Trans. Program. Lang. Syst., 2008

Flexible Immutability with Frozen Objects.

K. Rustan M. Leino, Peter Müller, Angela Wallenburg

Proceedings of the Verified Software: Theories, 2008

HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier.

Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs.

K. Rustan M. Leino, Peter Müller

Proceedings of the Advanced Lectures on Software Engineering, 2008

Class-local object invariants.

K. Rustan M. Leino, Angela Wallenburg

Proceedings of the Proceeding of the 1st Annual India Software Engineering Conference, 2008

Verification of Equivalent-Results Methods.

K. Rustan M. Leino, Peter Müller

Proceedings of the Programming Languages and Systems, 2008

Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software Engineering.

K. Rustan M. Leino

Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference, 2008

2007

Specification and verification challenges for sequential object-oriented programs.

Gary T. Leavens, K. Rustan M. Leino, Peter Müller

Formal Aspects Comput., 2007

Verifying Object-Oriented Software: Lessons and Challenges.

K. Rustan M. Leino

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Specifying and verifying software.

K. Rustan M. Leino

Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007), 2007

Practical Reasoning About Invocations and Implementations of Pure Methods.

Ádám Darvas, K. Rustan M. Leino

Proceedings of the Fundamental Approaches to Software Engineering, 2007

Using History Invariants to Verify Observers.

K. Rustan M. Leino, Wolfram Schulte

Proceedings of the Programming Languages and Systems, 2007

Designing Verification Conditions for Software.

K. Rustan M. Leino

Proceedings of the Automated Deduction, 2007

2006

A Verification Methodology for Model Fields.

K. Rustan M. Leino, Peter Müller

Proceedings of the Programming Languages and Systems, 2006

Specifying and Verifying Programs in Spec#.

K. Rustan M. Leino

Proceedings of the Perspectives of Systems Informatics, 2006

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

Generating error traces from verification-condition counterexamples.

K. Rustan M. Leino, Todd D. Millstein, James B. Saxe

Sci. Comput. Program., 2005

Efficient weakest preconditions.

K. Rustan M. Leino

Inf. Process. Lett., 2005

Inferring Object Invariants: Extended Abstract.

Bor-Yuh Evan Chang, K. Rustan M. Leino

Proceedings of the First International Workshop on Abstract Interpretation of Object-oriented Languages, 2005

The Spec# Programming System: Challenges and Directions.

Michael Barnett, Robert DeLine, Manuel Fähndrich, Bart Jacobs, K. Rustan M. Leino, Wolfram Schulte, Herman Venter

Proceedings of the Verified Software: Theories, 2005

Abstract Interpretation with Alien Expressions and Heap Structures.

Bor-Yuh Evan Chang, K. Rustan M. Leino

Proceedings of the Verification, 2005

A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover.

K. Rustan M. Leino, Madan Musuvathi, Xinming Ou

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Invariants on Demand.

K. Rustan M. Leino

Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 2005

Safe Concurrency for Aggregate Objects with Invariants.

Bart Jacobs, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte

Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 2005

Weakest-precondition of unstructured programs.

Michael Barnett, K. Rustan M. Leino

Proceedings of the 2005 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, 2005

Boogie: A Modular Reusable Verifier for Object-Oriented Programs.

Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, K. Rustan M. Leino

Proceedings of the Formal Methods for Components and Objects, 4th International Symposium, 2005

Modular Verification of Static Class Invariants.

K. Rustan M. Leino, Peter Müller

Proceedings of the FM 2005: Formal Methods, 2005

Program Verification and Programming Methodology.

K. Rustan M. Leino

Proceedings of the 12th International Workshop on Abstract State Machines, 2005

Loop Invariants on Demand.

K. Rustan M. Leino, Francesco Logozzo

Proceedings of the Programming Languages and Systems, Third Asian Symposium, 2005

2004

Verification of Object-Oriented Programs with Invariants.

Michael Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte

J. Object Technol., 2004

On computing the fixpoint of a set of boolean equations

Viktor Kuncak, K. Rustan M. Leino

CoRR, 2004

Finding stale-value errors in concurrent programs.

Michael Burrows, K. Rustan M. Leino

Concurr. Pract. Exp., 2004

Exception Safety for C#.

K. Rustan M. Leino, Wolfram Schulte

Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004

Challenges in Increasing Tool Support for Programming.

K. Rustan M. Leino

Proceedings of the Theoretical Aspects of Computing, 2004

Object Invariants in Dynamic Contexts.

K. Rustan M. Leino, Peter Müller

Proceedings of the ECOOP 2004, 2004

The Spec# Programming System: An Overview.

Mike Barnett, K. Rustan M. Leino, Wolfram Schulte

Proceedings of the Construction and Analysis of Safe, 2004

2003

A SAT Characterization of Boolean-Program Correctness.

K. Rustan M. Leino

Proceedings of the Model Checking Software, 2003

Declaring and checking non-null types in an object-oriented language.

Manuel Fähndrich, K. Rustan M. Leino

Proceedings of the 2003 ACM SIGPLAN Conference on Object-Oriented Programming Systems, 2003

A Logic of Object-Oriented Programs.

Martín Abadi, K. Rustan M. Leino

Proceedings of the Verification: Theory and Practice, 2003

2002

Data abstraction and information hiding.

K. Rustan M. Leino, Greg Nelson

ACM Trans. Program. Lang. Syst., 2002

Using Data Groups to Specify and Check Side Effects.

K. Rustan M. Leino, Arnd Poetzsch-Heffter, Yunhong Zhou

Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2002

Extended Static Checking for Java.

Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata

Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2002

2001

Real estate of names.

K. Rustan M. Leino

Inf. Process. Lett., 2001

Annotation inference for modular checkers.

Cormac Flanagan, Rajeev Joshi, K. Rustan M. Leino

Inf. Process. Lett., 2001

Applications of Extended Static Checking.

K. Rustan M. Leino

Proceedings of the Static Analysis, 8th International Symposium, 2001

Houdini, an Annotation Assistant for ESC/Java.

Cormac Flanagan, K. Rustan M. Leino

Proceedings of the FME 2001: Formal Methods for Increasing Software Productivity, 2001

Extended Static Checking: A Ten-Year Perspective.

K. Rustan M. Leino

Proceedings of the Informatics - 10 Years Back. 10 Years Ahead., 2001

2000

A semantic approach to secure information flow.

Rajeev Joshi, K. Rustan M. Leino

Sci. Comput. Program., 2000

JML (poster session): notations and tools supporting detailed design in Java.

Gary T. Leavens, Clyde Ruby, K. Rustan M. Leino, Erik Poll, Bart Jacobs

Proceedings of the Addendum to the 2000 Proceedings of the Conference on Object-Oriented Programming Systems, 2000

1999

Joining Specification Statements.

K. Rustan M. Leino, Rajit Manohar

Theor. Comput. Sci., 1999

Virginity: A Contribution to the Specification of Object-Oriented Software.

K. Rustan M. Leino, Raymie Stata

Inf. Process. Lett., 1999

Computing Permutation Encodings.

K. Rustan M. Leino

Formal Aspects Comput., 1999

Checking Java Programs via Guarded Commands.

K. Rustan M. Leino, James B. Saxe, Raymie Stata

Proceedings of the Object-Oriented Technology, ECOOP'99 Workshop Reader, 1999

1998

Recursive Object Types in a Logic of Object-Oriented Programs.

K. Rustan M. Leino

Nord. J. Comput., 1998

Extended static checking.

K. Rustan M. Leino

Proceedings of the Programming Concepts and Methods, 1998

Data Groups: Specifying the Modification of Extended State.

K. Rustan M. Leino

Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, 1998

An Extended Static Checker for Modular-3.

K. Rustan M. Leino, Greg Nelson

Proceedings of the Compiler Construction, 7th International Conference, 1998

1995

Toward reliable modular programs.

K. Rustan M. Leino

PhD thesis, 1995

Constructing a Program with Exceptions.

K. Rustan M. Leino

Inf. Process. Lett., 1995

Conditional Composition.

Rajit Manohar, K. Rustan M. Leino

Formal Aspects Comput., 1995

A Method for Showing Progress.

K. Rustan M. Leino

Formal Aspects Comput., 1995

1994

Semantics of Exceptions.

K. Rustan M. Leino, Jan L. A. van de Snepscheut

Proceedings of the Programming Concepts, 1994