K. Rustan M. Leino

ORCID

Publication Activity (10 Years)

Years Active: 1994-2022
Publications (10 Years): 8

Top Venues

CAV (1)

VMCAI

VSTTE

Publications

David R. Cok, K. Rustan M. Leino
Specifying the Boundary Between Unverified and Verified Code. The Logic of Software. A Tasting Menu of Formal Methods (2022)
K. Rustan M. Leino, Daniel Matichuk
Modular Verification Scopes via Export Sets and Translucent Exports. Principled Software Development (2018)
Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath T. V. Setty, Laure Thompson
Vale: Verifying High-Performance Cryptographic Assembly Code. USENIX Security Symposium (2017)
K. Rustan M. Leino
Modeling Concurrency in Dafny. SETSS (2017)
K. Rustan M. Leino
Accessible Software Verification with Dafny. IEEE Softw. 34 (6) (2017)
Maria Christakis, K. Rustan M. Leino, Peter Müller, Valentin Wüstholz
Integrated Environment for Diagnosing Verification Errors. TACAS (2016)
Razvan Certezeanu, Sophia Drossopoulou, Benjamin Egelund-Müller, K. Rustan M. Leino, Sinduran Sivarajan, Mark J. Wheelhouse
Quicksort Revisited - Verifying Alternative Versions of Quicksort. Theory and Practice of Formal Methods (2016)
K. Rustan M. Leino, Clément Pit-Claudel
Trigger Selection Strategies to Stabilize Program Verifiers. CAV (1) (2016)
K. Rustan M. Leino, Paqui Lucio
An Assertional Proof of the Stability and Correctness of Natural Mergesort. ACM Trans. Comput. Log. 17 (1) (2015)
K. Rustan M. Leino
Compiling Hilbert's epsilon operator. LPAR (short papers) (2015)
Reza Ahmadi, K. Rustan M. Leino, Jyrki Nummenmaa
Automatic verification of Dafny programs with traits. FTfJP@ECOOP (2015)
Jason Koenig, K. Rustan M. Leino
Programming Language Features for Refinement. Refine@FM (2015)
K. Rustan M. Leino, Valentin Wüstholz
Fine-Grained Caching of Verification Results. CAV (1) (2015)
Nada Amin, K. Rustan M. Leino, Tiark Rompf
Computing with an SMT Solver. TAP@STAF (2014)
K. Rustan M. Leino, Valentin Wüstholz
The Dafny Integrated Development Environment. F-IDE (2014)
Maria Christakis, K. Rustan M. Leino, Wolfram Schulte
Formalizing and Verifying a Modern Build Language. FM (2014)
K. Rustan M. Leino, Michal Moskal
Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier. FM (2014)
K. Rustan M. Leino
Automating Theorem Proving with SMT. ITP (2013)
Parosh Aziz Abdulla, K. Rustan M. Leino
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. 15 (2) (2013)
Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata
PLDI 2002: Extended static checking for Java. ACM SIGPLAN Notices 48 (4S) (2013)
K. Rustan M. Leino, Nadia Polikarpova
Verified Calculations. VSTTE (2013)
Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers
Abstract Read Permissions: Fractional Permissions without the Fractions. VMCAI (2013)
K. Rustan M. Leino
Developing verified programs with dafny. ICSE (2013)
K. Rustan M. Leino, Kuat Yessenov
Stepwise refinement of heap-manipulating code in Chalice. Formal Aspects Comput. 24 (4-6) (2012)
K. Rustan M. Leino
Developing verified programs with Dafny. HILT (2012)
John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew J. Parkinson
Behavioral interface specification languages. ACM Comput. Surv. 44 (3) (2012)
K. Rustan M. Leino
Staged program development. SPLASH (2012)
K. Rustan M. Leino
Developing Verified Programs with Dafny. VSTTE (2012)
K. Rustan M. Leino
Program proving using intermediate verification languages (IVLs) like boogie and why3. HILT (2012)
K. Rustan M. Leino
Automating Induction with an SMT Solver. VMCAI (2012)
K. Rustan M. Leino, Aleksandar Milicevic
Program extrapolation with jennisys. OOPSLA (2012)
Néstor Cataño, K. Rustan M. Leino, Víctor Rivera
The EventB2Dafny rodin plug-in. TOPI@ICSE (2012)
Claire Le Goues, K. Rustan M. Leino, Michal Moskal
The Boogie Verification Debugger (Tool Paper). SEFM (2011)
Mike 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) (2011)
K. Rustan M. Leino
From Retrospective Verification to Forward-Looking Development. NASA Formal Methods (2011)
Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers
Fractional permissions without the fractions. FTfJP@ECOOP (2011)
Luke Herbert, K. Rustan M. Leino, Jose Quaresma
Using Dafny, an Automatic Program Verifier. LASER Summer School (2011)
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ß
The 1st Verified Software Competition: Experience Report. FM (2011)
K. Rustan M. Leino
Tools and Behavioral Abstraction: A Direction for Software Engineering. The Future of Software Engineering (2010)
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies
Doomed program points. Formal Methods Syst. Des. 37 (2-3) (2010)
K. Rustan M. Leino
Dafny: An Automatic Program Verifier for Functional Correctness. LPAR (Dakar) (2010)
K. Rustan M. Leino
Verifying Concurrent Programs with Chalice. VMCAI (2010)
K. Rustan M. Leino
Learning to do program verification. Commun. ACM 53 (6) (2010)
Michael Barnett, K. Rustan M. Leino
To Goto Where No Statement Has Gone Before. VSTTE (2010)
K. Rustan M. Leino, Peter Müller, Jan Smans
Deadlock-Free Channels and Locks. ESOP (2010)
K. Rustan M. Leino, Philipp Rümmer
A Polymorphic Intermediate Verification Language: Design and Logical Encoding. TACAS (2010)
K. Rustan M. Leino, Rosemary Monahan
Dafny Meets the Verification Benchmarks Challenge. VSTTE (2010)
K. Rustan M. Leino, Peter Müller, Jan Smans
Verification of Concurrent Programs with Chalice. FOSAD (2009)
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies
It's Doomed; We Can Prove It. FM (2009)
K. Rustan M. Leino, Ronald Middelkoop
Proving Consistency of Pure Methods and Model Fields. FASE (2009)
K. Rustan M. Leino, Rosemary Monahan
Reasoning about comprehensions with first-order SMT solvers. SAC (2009)
K. Rustan M. Leino, Peter Müller
A Basis for Verifying Multi-threaded Programs. ESOP (2009)
K. Rustan M. Leino
Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software Engineering. COMPSAC (2008)
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)
K. Rustan M. Leino, Peter Müller
Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs. LASER Summer School (2008)
K. Rustan M. Leino, Peter Müller
Verification of Equivalent-Results Methods. ESOP (2008)
K. Rustan M. Leino, Peter Müller, Angela Wallenburg
Flexible Immutability with Frozen Objects. VSTTE (2008)
K. Rustan M. Leino, Angela Wallenburg
Class-local object invariants. ISEC (2008)
Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff
HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier. TPHOLs (2008)
K. Rustan M. Leino
Specifying and verifying software. ASE (2007)
K. Rustan M. Leino
Designing Verification Conditions for Software. CADE (2007)
Ádám Darvas, K. Rustan M. Leino
Practical Reasoning About Invocations and Implementations of Pure Methods. FASE (2007)
Gary T. Leavens, K. Rustan M. Leino, Peter Müller
Specification and verification challenges for sequential object-oriented programs. Formal Aspects Comput. 19 (2) (2007)
K. Rustan M. Leino
Verifying Object-Oriented Software: Lessons and Challenges. TACAS (2007)
K. Rustan M. Leino, Wolfram Schulte
Using History Invariants to Verify Observers. ESOP (2007)
K. Rustan M. Leino
Specifying and Verifying Programs in Spec#. Ershov Memorial Conference (2006)
K. Rustan M. Leino, Peter Müller
A Verification Methodology for Model Fields. ESOP (2006)
Bor-Yuh Evan Chang, K. Rustan M. Leino
Abstract Interpretation with Alien Expressions and Heap Structures. VMCAI (2005)
Bart Jacobs, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte
Safe Concurrency for Aggregate Objects with Invariants. SEFM (2005)
K. Rustan M. Leino
Invariants on Demand. SEFM (2005)
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)
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)
K. Rustan M. Leino, Madan Musuvathi, Xinming Ou
A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover. TACAS (2005)
K. Rustan M. Leino, Todd D. Millstein, James B. Saxe
Generating error traces from verification-condition counterexamples. Sci. Comput. Program. 55 (1-3) (2005)
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. Int. J. Softw. Tools Technol. Transf. 7 (3) (2005)
K. Rustan M. Leino, Francesco Logozzo
Loop Invariants on Demand. APLAS (2005)
Michael Barnett, K. Rustan M. Leino
Weakest-precondition of unstructured programs. PASTE (2005)
K. Rustan M. Leino
Program Verification and Programming Methodology. Abstract State Machines (2005)
K. Rustan M. Leino, Peter Müller
Modular Verification of Static Class Invariants. FM (2005)
Bor-Yuh Evan Chang, K. Rustan M. Leino
Inferring Object Invariants: Extended Abstract. Electron. Notes Theor. Comput. Sci. 131 (2005)
K. Rustan M. Leino
Efficient weakest preconditions. Inf. Process. Lett. 93 (6) (2005)
Viktor Kuncak, K. Rustan M. Leino
On computing the fixpoint of a set of boolean equations CoRR (2004)
K. Rustan M. Leino, Wolfram Schulte
Exception Safety for C#. SEFM (2004)
Michael Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte
Verification of Object-Oriented Programs with Invariants. J. Object Technol. 3 (6) (2004)
Mike Barnett, K. Rustan M. Leino, Wolfram Schulte
The Spec# Programming System: An Overview. CASSIS (2004)
K. Rustan M. Leino, Peter Müller
Object Invariants in Dynamic Contexts. ECOOP (2004)
K. Rustan M. Leino
Challenges in Increasing Tool Support for Programming. ICTAC (2004)
Michael Burrows, K. Rustan M. Leino
Finding stale-value errors in concurrent programs. Concurr. Pract. Exp. 16 (12) (2004)
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. Electron. Notes Theor. Comput. Sci. 80 (2003)
K. Rustan M. Leino
A SAT Characterization of Boolean-Program Correctness. SPIN (2003)
Martín Abadi, K. Rustan M. Leino
A Logic of Object-Oriented Programs. Verification: Theory and Practice (2003)
Manuel Fähndrich, K. Rustan M. Leino
Declaring and checking non-null types in an object-oriented language. OOPSLA (2003)
K. Rustan M. Leino, Arnd Poetzsch-Heffter, Yunhong Zhou
Using Data Groups to Specify and Check Side Effects. PLDI (2002)
Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata
Extended Static Checking for Java. PLDI (2002)
K. Rustan M. Leino, Greg Nelson
Data abstraction and information hiding. ACM Trans. Program. Lang. Syst. 24 (5) (2002)
K. Rustan M. Leino
Extended Static Checking: A Ten-Year Perspective. Informatics (2001)
K. Rustan M. Leino
Applications of Extended Static Checking. SAS (2001)
Cormac Flanagan, Rajeev Joshi, K. Rustan M. Leino
Annotation inference for modular checkers. Inf. Process. Lett. 77 (2-4) (2001)
Cormac Flanagan, K. Rustan M. Leino
Houdini, an Annotation Assistant for ESC/Java. FME (2001)
K. Rustan M. Leino
Real estate of names. Inf. Process. Lett. 77 (2-4) (2001)

K. Rustan M. Leino.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

K. Rustan M. Leino