default search action
K. Rustan M. Leino
Person information
- affiliation: Amazon Web Services
- affiliation (former): Microsoft Research
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j28]Aws Albarghouthi, K. Rustan M. Leino, Alexandra Silva, Caterina Urban:
Preface of the special issue on the conference on Computer-Aided Verification 2020 and 2021. Formal Methods Syst. Des. 63(1): 1-4 (2024) - [c92]Tabea Bordis
, K. Rustan M. Leino
Free Facts: An Alternative to Inefficient Axioms in Dafny. FM (1) 2024: 151-169 - 2022
- [c91]David R. Cok
Specifying the Boundary Between Unverified and Verified Code. The Logic of Software. A Tasting Menu of Formal Methods 2022: 105-128 - 2021
- [e4]Alexandra Silva, K. Rustan M. Leino:
Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I. Lecture Notes in Computer Science 12759, Springer 2021, ISBN 978-3-030-81684-1 [contents] - [e3]Alexandra Silva, K. Rustan M. Leino:
Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. Lecture Notes in Computer Science 12760, Springer 2021, ISBN 978-3-030-81687-2 [contents]
2010 – 2019
- 2018
- [c90]K. Rustan M. Leino, Daniel Matichuk:
Modular Verification Scopes via Export Sets and Translucent Exports. Principled Software Development 2018: 185-202 - 2017
- [j27]K. Rustan M. Leino:
Accessible Software Verification with Dafny. IEEE Softw. 34(6): 94-97 (2017) - [c89]K. Rustan M. Leino
Modeling Concurrency in Dafny. SETSS 2017: 115-142 - [c88]Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss
Everest: Towards a Verified, Drop-in Replacement of HTTPS. SNAPL 2017: 1:1-1:12 - [c87]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: 917-934 - 2016
- [c86]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: 407-426 - [c85]K. Rustan M. Leino, Clément Pit-Claudel
Trigger Selection Strategies to Stabilize Program Verifiers. CAV (1) 2016: 361-381 - [c84]Maria Christakis, K. Rustan M. Leino, Peter Müller, Valentin Wüstholz:
Integrated Environment for Diagnosing Verification Errors. TACAS 2016: 424-441 - [e2]Barbara Jobstmann, K. Rustan M. Leino:
Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings. Lecture Notes in Computer Science 9583, Springer 2016, ISBN 978-3-662-49121-8 [contents] - 2015
- [j26]K. Rustan M. Leino, Paqui Lucio
An Assertional Proof of the Stability and Correctness of Natural Mergesort. ACM Trans. Comput. Log. 17(1): 6 (2015) - [c83]K. Rustan M. Leino, Valentin Wüstholz:
Fine-Grained Caching of Verification Results. CAV (1) 2015: 380-397 - [c82]Reza Ahmadi, K. Rustan M. Leino, Jyrki Nummenmaa
Automatic verification of Dafny programs with traits. FTfJP@ECOOP 2015: 4:1-4:5 - [c81]K. Rustan M. Leino:
Well-founded Functions and Extreme Predicates in Dafny: A Tutorial. IWIL@LPAR 2015: 52-66 - [c80]K. Rustan M. Leino:
Compiling Hilbert's epsilon operator. LPAR (short papers) 2015: 106-118 - [c79]Jason Koenig, K. Rustan M. Leino:
Programming Language Features for Refinement. Refine@FM 2015: 87-106 - 2014
- [c78]K. Rustan M. Leino, Michal Moskal:
Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier. FM 2014: 382-398 - [c77]Maria Christakis, K. Rustan M. Leino, Wolfram Schulte:
Formalizing and Verifying a Modern Build Language. FM 2014: 643-657 - [c76]Nada Amin, K. Rustan M. Leino, Tiark Rompf:
Computing with an SMT Solver. TAP@STAF 2014: 20-35 - [c75]K. Rustan M. Leino, Valentin Wüstholz:
The Dafny Integrated Development Environment. F-IDE 2014: 3-15 - 2013
- [j25]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): 22-33 (2013) - [j24]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): 85-88 (2013) - [c74]K. Rustan M. Leino:
Developing verified programs with dafny. ICSE 2013: 1488-1490 - [c73]K. Rustan M. Leino:
Automating Theorem Proving with SMT. ITP 2013: 2-16 - [c72]Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers:
Abstract Read Permissions: Fractional Permissions without the Fractions. VMCAI 2013: 315-334 - [c71]K. Rustan M. Leino, Nadia Polikarpova:
Verified Calculations. VSTTE 2013: 170-190 - 2012
- [j23]John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew J. Parkinson:
Behavioral interface specification languages. ACM Comput. Surv. 44(3): 16:1-16:58 (2012) - [j22]K. Rustan M. Leino, Kuat Yessenov:
Stepwise refinement of heap-manipulating code in Chalice. Formal Aspects Comput. 24(4-6): 519-535 (2012) - [c70]Néstor Cataño
The EventB2Dafny rodin plug-in. TOPI@ICSE 2012: 49-54 - [c69]K. Rustan M. Leino:
Staged program development. SPLASH 2012: 3-4 - [c68]K. Rustan M. Leino, Aleksandar Milicevic:
Program extrapolation with jennisys. OOPSLA 2012: 411-430 - [c67]K. Rustan M. Leino:
Developing verified programs with Dafny. HILT 2012: 9-10 - [c66]K. Rustan M. Leino:
Program proving using intermediate verification languages (IVLs) like boogie and why3. HILT 2012: 25-26 - [c65]K. Rustan M. Leino:
Automating Induction with an SMT Solver. VMCAI 2012: 315-331 - [c64]K. Rustan M. Leino:
Developing Verified Programs with Dafny. VSTTE 2012: 82 - [p1]Jason Koenig, K. Rustan M. Leino:
Getting Started with Dafny: A Guide. Software Safety and Security 2012: 152-181 - 2011
- [j21]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): 81-91 (2011) - [c63]Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers:
Fractional permissions without the fractions. FTfJP@ECOOP 2011: 1:1-1:6 - [c62]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
The 1st Verified Software Competition: Experience Report. FM 2011: 154-168 - [c61]Luke Herbert, K. Rustan M. Leino, Jose Quaresma:
Using Dafny, an Automatic Program Verifier. LASER Summer School 2011: 156-181 - [c60]K. Rustan M. Leino:
From Retrospective Verification to Forward-Looking Development. NASA Formal Methods 2011: 1 - [c59]Claire Le Goues
The Boogie Verification Debugger (Tool Paper). SEFM 2011: 407-414 - [e1]Parosh Aziz Abdulla, K. Rustan M. Leino:
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. Lecture Notes in Computer Science 6605, Springer 2011, ISBN 978-3-642-19834-2 [contents] - 2010
- [j20]K. Rustan M. Leino:
Learning to do program verification. Commun. ACM 53(6): 106 (2010) - [j19]Jochen Hoenicke
Doomed program points. Formal Methods Syst. Des. 37(2-3): 171-199 (2010) - [c58]K. Rustan M. Leino:
Tools and Behavioral Abstraction: A Direction for Software Engineering. The Future of Software Engineering 2010: 115-124 - [c57]K. Rustan M. Leino, Peter Müller, Jan Smans:
Deadlock-Free Channels and Locks. ESOP 2010: 407-426 - [c56]K. Rustan M. Leino:
Dafny: An Automatic Program Verifier for Functional Correctness. LPAR (Dakar) 2010: 348-370 - [c55]K. Rustan M. Leino, Philipp Rümmer:
A Polymorphic Intermediate Verification Language: Design and Logical Encoding. TACAS 2010: 312-327 - [c54]K. Rustan M. Leino:
Verifying Concurrent Programs with Chalice. VMCAI 2010: 2 - [c53]K. Rustan M. Leino, Rosemary Monahan
Dafny Meets the Verification Benchmarks Challenge. VSTTE 2010: 112-126 - [c52]Michael Barnett, K. Rustan M. Leino:
To Goto Where No Statement Has Gone Before. VSTTE 2010: 157-168
2000 – 2009
- 2009
- [c51]K. Rustan M. Leino, Peter Müller:
A Basis for Verifying Multi-threaded Programs. ESOP 2009: 378-393 - [c50]K. Rustan M. Leino, Ronald Middelkoop:
Proving Consistency of Pure Methods and Model Fields. FASE 2009: 231-245 - [c49]Jochen Hoenicke
It's Doomed; We Can Prove It. FM 2009: 338-353 - [c48]K. Rustan M. Leino, Peter Müller, Jan Smans:
Verification of Concurrent Programs with Chalice. FOSAD 2009: 195-222 - [c47]K. Rustan M. Leino, Rosemary Monahan
Reasoning about comprehensions with first-order SMT solvers. SAC 2009: 615-622 - 2008
- [j18]Bart Jacobs
A programming model for concurrent object-oriented programs. ACM Trans. Program. Lang. Syst. 31(1): 1:1-1:48 (2008) - [c46]K. Rustan M. Leino:
Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software Engineering. COMPSAC 2008: 11 - [c45]K. Rustan M. Leino, Peter Müller:
Verification of Equivalent-Results Methods. ESOP 2008: 307-321 - [c44]K. Rustan M. Leino, Angela Wallenburg:
Class-local object invariants. ISEC 2008: 57-66 - [c43]K. Rustan M. Leino, Peter Müller:
Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs. LASER Summer School 2008: 91-139 - [c42]Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff:
HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier. TPHOLs 2008: 150-166 - [c41]K. Rustan M. Leino, Peter Müller, Angela Wallenburg:
Flexible Immutability with Frozen Objects. VSTTE 2008: 192-208 - 2007
- [j17]Gary T. Leavens, K. Rustan M. Leino, Peter Müller:
Specification and verification challenges for sequential object-oriented programs. Formal Aspects Comput. 19(2): 159-189 (2007) - [c40]K. Rustan M. Leino:
Designing Verification Conditions for Software. CADE 2007: 345 - [c39]K. Rustan M. Leino, Wolfram Schulte:
Using History Invariants to Verify Observers. ESOP 2007: 80-94 - [c38]Ádám Darvas, K. Rustan M. Leino:
Practical Reasoning About Invocations and Implementations of Pure Methods. FASE 2007: 336-351 - [c37]K. Rustan M. Leino:
Specifying and verifying software. ASE 2007: 2 - [c36]K. Rustan M. Leino:
Verifying Object-Oriented Software: Lessons and Challenges. TACAS 2007: 2 - 2006
- [c35]K. Rustan M. Leino:
Specifying and Verifying Programs in Spec#. Ershov Memorial Conference 2006: 20 - [c34]K. Rustan M. Leino, Peter Müller:
A Verification Methodology for Model Fields. ESOP 2006: 115-130 - 2005
- [j16]K. Rustan M. Leino:
Efficient weakest preconditions. Inf. Process. Lett. 93(6): 281-288 (2005) - [j15]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) - [j14]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): 212-232 (2005) - [c33]K. Rustan M. Leino, Francesco Logozzo:
Loop Invariants on Demand. APLAS 2005: 119-134 - [c32]K. Rustan M. Leino:
Program Verification and Programming Methodology. Abstract State Machines 2005: 73 - [c31]K. Rustan M. Leino, Peter Müller:
Modular Verification of Static Class Invariants. FM 2005: 26-42 - [c30]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 - [c29]Michael Barnett, K. Rustan M. Leino:
Weakest-precondition of unstructured programs. PASTE 2005: 82-87 - [c28]Bart Jacobs
Safe Concurrency for Aggregate Objects with Invariants. SEFM 2005: 137-147 - [c27]K. Rustan M. Leino:
Invariants on Demand. SEFM 2005: 148-149 - [c26]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 - [c25]Bor-Yuh Evan Chang, K. Rustan M. Leino:
Abstract Interpretation with Alien Expressions and Heap Structures. VMCAI 2005: 147-163 - [c24]Michael Barnett, Robert DeLine, Manuel Fähndrich, Bart Jacobs
The Spec# Programming System: Challenges and Directions. VSTTE 2005: 144-152 - [c23]Bor-Yuh Evan Chang
Inferring Object Invariants: Extended Abstract. AIOOL@VMCAI 2005: 63-74 - 2004
- [j13]Michael Burrows, K. Rustan M. Leino:
Finding stale-value errors in concurrent programs. Concurr. Pract. Exp. 16(12): 1161-1172 (2004) - [j12]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): 27-56 (2004) - [c22]Mike Barnett, K. Rustan M. Leino, Wolfram Schulte:
The Spec# Programming System: An Overview. CASSIS 2004: 49-69 - [c21]K. Rustan M. Leino, Peter Müller:
Object Invariants in Dynamic Contexts. ECOOP 2004: 491-516 - [c20]K. Rustan M. Leino:
Challenges in Increasing Tool Support for Programming. ICTAC 2004: 35-35 - [c19]K. Rustan M. Leino, Wolfram Schulte:
Exception Safety for C#. SEFM 2004: 218-227 - [i1]Viktor Kuncak, K. Rustan M. Leino:
On computing the fixpoint of a set of boolean equations. CoRR cs.PL/0408045 (2004) - 2003
- [c18]Martín Abadi, K. Rustan M. Leino:
A Logic of Object-Oriented Programs. Verification: Theory and Practice 2003: 11-41 - [c17]Manuel Fähndrich, K. Rustan M. Leino:
Declaring and checking non-null types in an object-oriented language. OOPSLA 2003: 302-312 - [c16]K. Rustan M. Leino:
A SAT Characterization of Boolean-Program Correctness. SPIN 2003: 104-120 - [c15]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. FMICS 2003: 75-91 - 2002
- [j11]K. Rustan M. Leino, Greg Nelson:
Data abstraction and information hiding. ACM Trans. Program. Lang. Syst. 24(5): 491-553 (2002) - [c14]Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata:
Extended Static Checking for Java. PLDI 2002: 234-245 - [c13]K. Rustan M. Leino, Arnd Poetzsch-Heffter, Yunhong Zhou:
Using Data Groups to Specify and Check Side Effects. PLDI 2002: 246-257 - 2001
- [j10]Cormac Flanagan, Rajeev Joshi, K. Rustan M. Leino:
Annotation inference for modular checkers. Inf. Process. Lett. 77(2-4): 97-108 (2001) - [j9]K. Rustan M. Leino:
Real estate of names. Inf. Process. Lett. 77(2-4): 169-171 (2001) - [c12]K. Rustan M. Leino:
Extended Static Checking: A Ten-Year Perspective. Informatics 2001: 157-175 - [c11]Cormac Flanagan, K. Rustan M. Leino:
Houdini, an Annotation Assistant for ESC/Java. FME 2001: 500-517 - [c10]K. Rustan M. Leino:
Applications of Extended Static Checking. SAS 2001: 185-193 - 2000
- [j8]Rajeev Joshi, K. Rustan M. Leino:
A semantic approach to secure information flow. Sci. Comput. Program. 37(1-3): 113-138 (2000) - [c9]Gary T. Leavens, Clyde Ruby, K. Rustan M. Leino, Erik Poll, Bart Jacobs:
JML (poster session): notations and tools supporting detailed design in Java. OOPSLA Addendum 2000: 105-106
1990 – 1999
- 1999
- [j7]K. Rustan M. Leino:
Computing Permutation Encodings. Formal Aspects Comput. 11(1): 56-74 (1999) - [j6]K. Rustan M. Leino, Raymie Stata:
Virginity: A Contribution to the Specification of Object-Oriented Software. Inf. Process. Lett. 70(2): 99-105 (1999) - [j5]K. Rustan M. Leino, Rajit Manohar:
Joining Specification Statements. Theor. Comput. Sci. 216(1-2): 375-394 (1999) - [c8]K. Rustan M. Leino, James B. Saxe, Raymie Stata:
Checking Java Programs via Guarded Commands. ECOOP Workshops 1999: 110-111 - 1998
- [j4]K. Rustan M. Leino:
Recursive Object Types in a Logic of Object-Oriented Programs. Nord. J. Comput. 5(4): 330-360 (1998) - [c7]K. Rustan M. Leino, Greg Nelson:
An Extended Static Checker for Modular-3. CC 1998: 302-305 - [c6]K. Rustan M. Leino:
Recursive Object Types in a Logic of Object-Oriented Programs. ESOP 1998: 170-184 - [c5]K. Rustan M. Leino, Rajeev Joshi:
A Semantic Approach to Secure Information Flow. MPC 1998: 254-271 - [c4]K. Rustan M. Leino:
Data Groups: Specifying the Modification of Extended State. OOPSLA 1998: 144-153 - [c3]K. Rustan M. Leino:
Extended static checking. PROCOMET 1998: 1-2 - 1997
- [c2]Martín Abadi, K. Rustan M. Leino:
A Logic of Object-Oriented Programs. TAPSOFT 1997: 682-696 - 1995
- [b1]K. Rustan M. Leino:
Toward reliable modular programs. California Institute of Technology, USA, 1995 - [j3]K. Rustan M. Leino:
A Method for Showing Progress. Formal Aspects Comput. 7(5): 576-580 (1995) - [j2]Rajit Manohar, K. Rustan M. Leino:
Conditional Composition. Formal Aspects Comput. 7(6): 683-703 (1995) - [j1]K. Rustan M. Leino:
Constructing a Program with Exceptions. Inf. Process. Lett. 53(3): 159-163 (1995) - 1994
- [c1]K. Rustan M. Leino, Jan L. A. van de Snepscheut:
Semantics of Exceptions. PROCOMET 1994: 447-466
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-31 21:10 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: