Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDK. 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
- 2022
[c91]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: 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, 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:
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, K. Rustan M. Leino, Víctor Rivera:
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, 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: 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, K. Rustan M. Leino, Michal Moskal:
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, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies:
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, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies:
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, 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): 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, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte:
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, K. Rustan M. Leino, Wolfram Schulte, Herman Venter:
The Spec# Programming System: Challenges and Directions. VSTTE 2005: 144-152 - [c23]Bor-Yuh Evan Chang, K. Rustan M. Leino:
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
- [j3]K. Rustan M. Leino:
A Method for Showing Progress. Formal Aspects Comput. 7(5): 576-580 (1995) - [j2]