K. Rustan M. Leino
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
57
Venues
23
Active years
1998–2026
Best venue rank
A*
Where they publish
- BFM7 papers
- AESOP6 papers
- AOOPSLA5 papers
- ATACAS4 papers
- BVMCAI4 papers
- BSEFM4 papers
- A*ICSE3 papers
- AECOOP3 papers
- BLPAR3 papers
- BITP2 papers
- A*CAV2 papers
- BFASE2 papers
- A*PLDI2 papers
- BFMCAD1 paper
- CTAP1 paper
- MulticonferenceSAC1 paper
- BCOMPSAC1 paper
- ACADE1 paper
- BAPLAS1 paper
- CICTAC1 paper
- BSAS1 paper
- BCC1 paper
- BMPC1 paper
Papers
57 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | ITP | Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language. | Vladimir Gladshtein, K. Rustan M. Leino |
| 2025 | ICSE | Formally Verified Cloud-Scale Authorization. | 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, Clment 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, Taejoon Byun, Joshua M. Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, Yongwei Yuan |
| 2024 | FM | Free Facts: An Alternative to Inefficient Axioms in Dafny. | Tabea Bordis, K. Rustan M. Leino |
| 2024 | FMCAD | Writing Proofs in Dafny. | K. Rustan M. Leino |
| 2016 | CAV | Trigger Selection Strategies to Stabilize Program Verifiers. | K. Rustan M. Leino, Clment Pit-Claudel |
| 2016 | TACAS | Integrated Environment for Diagnosing Verification Errors. | Maria Christakis, K. Rustan M. Leino, Peter Mller, Valentin Wstholz |
| 2015 | CAV | Fine-Grained Caching of Verification Results. | K. Rustan M. Leino, Valentin Wstholz |
| 2015 | ECOOP | Automatic verification of Dafny programs with traits. | Reza Ahmadi, K. Rustan M. Leino, Jyrki Nummenmaa |
| 2015 | LPAR | Compiling Hilbert's epsilon operator. | K. Rustan M. Leino |
| 2015 | LPAR | Well-founded Functions and Extreme Predicates in Dafny: A Tutorial. | K. Rustan M. Leino |
| 2014 | FM | Formalizing and Verifying a Modern Build Language. | Maria Christakis, K. Rustan M. Leino, Wolfram Schulte |
| 2014 | FM | Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier. | K. Rustan M. Leino, Michal Moskal |
| 2014 | TAP | Computing with an SMT Solver. | Nada Amin, K. Rustan M. Leino, Tiark Rompf |
| 2013 | ICSE | Developing verified programs with dafny. | K. Rustan M. Leino |
| 2013 | ITP | Automating Theorem Proving with SMT. | K. Rustan M. Leino |
| 2013 | VMCAI | Abstract Read Permissions: Fractional Permissions without the Fractions. | Stefan Heule, K. Rustan M. Leino, Peter Mller, Alexander J. Summers |
| 2012 | ICSE | The EventB2Dafny rodin plug-in. | Nstor Catao, K. Rustan M. Leino, Vctor Rivera |
| 2012 | OOPSLA | Staged program development. | K. Rustan M. Leino |
| 2012 | OOPSLA | Program extrapolation with jennisys. | K. Rustan M. Leino, Aleksandar Milicevic |
| 2012 | VMCAI | Automating Induction with an SMT Solver. | K. Rustan M. Leino |
| 2011 | ECOOP | Fractional permissions without the fractions. | Stefan Heule, K. Rustan M. Leino, Peter Mller, Alexander J. Summers |
| 2011 | FM | The 1st Verified Software Competition: Experience Report. | Vladimir Klebanov, Peter Mller, Natarajan Shankar, Gary T. Leavens, Valentin Wstholz, 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 | SEFM | The Boogie Verification Debugger (Tool Paper). | Claire Le Goues, K. Rustan M. Leino, Michal Moskal |
| 2010 | ESOP | Deadlock-Free Channels and Locks. | K. Rustan M. Leino, Peter Mller, Jan Smans |
| 2010 | LPAR | Dafny: An Automatic Program Verifier for Functional Correctness. | K. Rustan M. Leino |
| 2010 | TACAS | A Polymorphic Intermediate Verification Language: Design and Logical Encoding. | K. Rustan M. Leino, Philipp Rmmer |
| 2010 | VMCAI | Verifying Concurrent Programs with Chalice. | K. Rustan M. Leino |
| 2009 | ESOP | A Basis for Verifying Multi-threaded Programs. | K. Rustan M. Leino, Peter Mller |
| 2009 | FASE | Proving Consistency of Pure Methods and Model Fields. | K. Rustan M. Leino, Ronald Middelkoop |
| 2009 | FM | It's Doomed; We Can Prove It. | Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schf, Thomas Wies |
| 2009 | SAC | Reasoning about comprehensions with first-order SMT solvers. | K. Rustan M. Leino, Rosemary Monahan |
| 2008 | COMPSAC | Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software Engineering. | K. Rustan M. Leino |
| 2008 | ESOP | Verification of Equivalent-Results Methods. | K. Rustan M. Leino, Peter Mller |
| 2007 | CADE | Designing Verification Conditions for Software. | K. Rustan M. Leino |
| 2007 | ESOP | Using History Invariants to Verify Observers. | K. Rustan M. Leino, Wolfram Schulte |
| 2007 | FASE | Practical Reasoning About Invocations and Implementations of Pure Methods. | dm Darvas, K. Rustan M. Leino |
| 2007 | TACAS | Verifying Object-Oriented Software: Lessons and Challenges. | K. Rustan M. Leino |
| 2006 | ESOP | A Verification Methodology for Model Fields. | K. Rustan M. Leino, Peter Mller |
| 2005 | APLAS | Loop Invariants on Demand. | K. Rustan M. Leino, Francesco Logozzo |
| 2005 | FM | Modular Verification of Static Class Invariants. | K. Rustan M. Leino, Peter Mller |
| 2005 | SEFM | Safe Concurrency for Aggregate Objects with Invariants. | Bart Jacobs, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte |
| 2005 | SEFM | Invariants on Demand. | K. Rustan M. Leino |
| 2005 | TACAS | A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover. | K. Rustan M. Leino, Madan Musuvathi, Xinming Ou |
| 2005 | VMCAI | Abstract Interpretation with Alien Expressions and Heap Structures. | Bor-Yuh Evan Chang, K. Rustan M. Leino |
| 2004 | ECOOP | Object Invariants in Dynamic Contexts. | K. Rustan M. Leino, Peter Mller |
| 2004 | ICTAC | Challenges in Increasing Tool Support for Programming. | K. Rustan M. Leino |
| 2004 | SEFM | Exception Safety for C#. | K. Rustan M. Leino, Wolfram Schulte |
| 2003 | OOPSLA | Declaring and checking non-null types in an object-oriented language. | Manuel Fhndrich, K. Rustan M. Leino |
| 2002 | PLDI | Extended Static Checking for Java. | Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata |
| 2002 | PLDI | Using Data Groups to Specify and Check Side Effects. | K. Rustan M. Leino, Arnd Poetzsch-Heffter, Yunhong Zhou |
| 2001 | FM | Houdini, an Annotation Assistant for ESC/Java. | Cormac Flanagan, K. Rustan M. Leino |
| 2001 | SAS | Applications of Extended Static Checking. | K. Rustan M. Leino |
| 2000 | OOPSLA | JML (poster session): notations and tools supporting detailed design in Java. | Gary T. Leavens, Clyde Ruby, K. Rustan M. Leino, Erik Poll, Bart Jacobs |
| 1998 | CC | An Extended Static Checker for Modular-3. | K. Rustan M. Leino, Greg Nelson |
| 1998 | ESOP | Recursive Object Types in a Logic of Object-Oriented Programs. | K. Rustan M. Leino |
| 1998 | MPC | A Semantic Approach to Secure Information Flow. | K. Rustan M. Leino, Rajeev Joshi |
| 1998 | OOPSLA | Data Groups: Specifying the Modification of Extended State. | K. Rustan M. Leino |