Stop the war!

Остановите войну!

for scientists:

default search action

combined dblp search
author search
venue search
publication search

ask others

K. Rustan M. Leino

> Home > Persons

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

Journal Articles

see FAQ

What is the meaning of the colors in the publication lists?

2017
[j27]
- view
  authority control:
- export record
  dblp key:
  - journals/software/Leino17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/software/Leino17
K. Rustan M. Leino:
Accessible Software Verification with Dafny. IEEE Softw. 34(6): 94-97 (2017)
2015
[j26]
- view
  authority control:
- export record
  dblp key:
  - journals/tocl/LeinoL15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/tocl/LeinoL15
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)
2013
[j25]
- view
  authority control:
- export record
  dblp key:
  - journals/sigplan/FlanaganLLNSS13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/sigplan/FlanaganLLNSS13
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]
- view
  authority control:
- export record
  dblp key:
  - journals/sttt/AbdullaL13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/sttt/AbdullaL13
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)
2012
[j23]
- view
  authority control:
- export record
  dblp key:
  - journals/csur/HatcliffLLMP12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/csur/HatcliffLLMP12
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]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/fac/LeinoY12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fac/LeinoY12
K. Rustan M. Leino, Kuat Yessenov:
Stepwise refinement of heap-manipulating code in Chalice. Formal Aspects Comput. 24(4-6): 519-535 (2012)
2011
[j21]
- view
  authority control:
- export record
  dblp key:
  - journals/cacm/BarnettFLMSV11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/cacm/BarnettFLMSV11
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)
2010
[j20]
- view
  authority control:
- export record
  dblp key:
  - journals/cacm/Leino10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/cacm/Leino10
K. Rustan M. Leino:
Learning to do program verification. Commun. ACM 53(6): 106 (2010)
[j19]
- view
  authority control:
- export record
  dblp key:
  - journals/fmsd/HoenickeLPSW10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/HoenickeLPSW10
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)
2008
[j18]
- view
  authority control:
- export record
  dblp key:
  - journals/toplas/JacobsPSLS08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/toplas/JacobsPSLS08
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)
2007
[j17]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/fac/LeavensLM07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fac/LeavensLM07
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)
2005
[j16]
- view
  authority control:
- export record
  dblp key:
  - journals/ipl/Leino05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/ipl/Leino05
K. Rustan M. Leino:
Efficient weakest preconditions. Inf. Process. Lett. 93(6): 281-288 (2005)
[j15]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/scp/LeinoMS05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/scp/LeinoMS05
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]
- view
  authority control:
- export record
  dblp key:
  - journals/sttt/BurdyCCEKLLP05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/sttt/BurdyCCEKLLP05
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)
2004
[j13]
- view
  authority control:
- export record
  dblp key:
  - journals/concurrency/BurrowsL04
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/concurrency/BurrowsL04
Michael Burrows, K. Rustan M. Leino:
Finding stale-value errors in concurrent programs. Concurr. Pract. Exp. 16(12): 1161-1172 (2004)
[j12]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/jot/BarnettDFLS04
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jot/BarnettDFLS04
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)
2002
[j11]
- view
  authority control:
- export record
  dblp key:
  - journals/toplas/LeinoN02
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/toplas/LeinoN02
K. Rustan M. Leino, Greg Nelson:
Data abstraction and information hiding. ACM Trans. Program. Lang. Syst. 24(5): 491-553 (2002)
2001
[j10]
- view
  authority control:
- export record
  dblp key:
  - journals/ipl/FlanaganJL01
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/ipl/FlanaganJL01
Cormac Flanagan, Rajeev Joshi, K. Rustan M. Leino:
Annotation inference for modular checkers. Inf. Process. Lett. 77(2-4): 97-108 (2001)
[j9]
- view
  authority control:
- export record
  dblp key:
  - journals/ipl/Leino01
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/ipl/Leino01
K. Rustan M. Leino:
Real estate of names. Inf. Process. Lett. 77(2-4): 169-171 (2001)
2000
[j8]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/scp/JoshiL00
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/scp/JoshiL00
Rajeev Joshi, K. Rustan M. Leino:
A semantic approach to secure information flow. Sci. Comput. Program. 37(1-3): 113-138 (2000)
1999
[j7]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/fac/Leino99
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fac/Leino99
K. Rustan M. Leino:
Computing Permutation Encodings. Formal Aspects Comput. 11(1): 56-74 (1999)
[j6]
- view
  authority control:
- export record
  dblp key:
  - journals/ipl/LeinoS99
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/ipl/LeinoS99
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]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/tcs/LeinoM99
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/tcs/LeinoM99
K. Rustan M. Leino, Rajit Manohar:
Joining Specification Statements. Theor. Comput. Sci. 216(1-2): 375-394 (1999)
1998
[j4]
- no documents available
  - no references & citations available
- export record
  dblp key:
  - journals/njc/Leino98
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/njc/Leino98
K. Rustan M. Leino:
Recursive Object Types in a Logic of Object-Oriented Programs. Nord. J. Comput. 5(4): 330-360 (1998)
1995
[j3]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/fac/Leino95
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fac/Leino95
K. Rustan M. Leino:
A Method for Showing Progress. Formal Aspects Comput. 7(5): 576-580 (1995)
[j2]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/fac/ManoharL95
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fac/ManoharL95
Rajit Manohar, K. Rustan M. Leino:
Conditional Composition. Formal Aspects Comput. 7(6): 683-703 (1995)
[j1]
- view
  authority control:
- export record
  dblp key:
  - journals/ipl/Leino95
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/ipl/Leino95
K. Rustan M. Leino:
Constructing a Program with Exceptions. Inf. Process. Lett. 53(3): 159-163 (1995)

Conference and Workshop Papers

see FAQ

What is the meaning of the colors in the publication lists?

2022
[c91]
- view
  authority control:
- export record
  dblp key:
  - conf/birthday/CokL20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/birthday/CokL20
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
2018
[c90]
- view
  authority control:
- export record
  dblp key:
  - conf/birthday/LeinoM18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/birthday/LeinoM18
K. Rustan M. Leino, Daniel Matichuk:
Modular Verification Scopes via Export Sets and Translucent Exports. Principled Software Development 2018: 185-202
2017
[c89]
- view
  authority control:
- export record
  dblp key:
  - conf/setss/Leino17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/setss/Leino17
K. Rustan M. Leino:
Modeling Concurrency in Dafny. SETSS 2017: 115-142
[c88]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/snapl/BhargavanBDFHHI17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/snapl/BhargavanBDFHHI17
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]
- view
  - electronic edition @ usenix.org (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/uss/BondHKLLPRST17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/uss/BondHKLLPRST17
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]
- view
  authority control:
- export record
  dblp key:
  - conf/birthday/CertezeanuDELSW16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/birthday/CertezeanuDELSW16
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]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/LeinoP16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/LeinoP16
K. Rustan M. Leino, Clément Pit-Claudel:
Trigger Selection Strategies to Stabilize Program Verifiers. CAV (1) 2016: 361-381
[c84]
- view
  authority control:
- export record
  dblp key:
  - conf/tacas/ChristakisL0W16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/ChristakisL0W16
Maria Christakis, K. Rustan M. Leino, Peter Müller, Valentin Wüstholz:
Integrated Environment for Diagnosing Verification Errors. TACAS 2016: 424-441
2015
[c83]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cav/LeinoW15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/LeinoW15
K. Rustan M. Leino, Valentin Wüstholz:
Fine-Grained Caching of Verification Results. CAV (1) 2015: 380-397
[c82]
- view
  authority control:
- export record
  dblp key:
  - conf/ecoop/AhmadiLN15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ecoop/AhmadiLN15
Reza Ahmadi, K. Rustan M. Leino, Jyrki Nummenmaa:
Automatic verification of Dafny programs with traits. FTfJP@ECOOP 2015: 4:1-4:5
[c81]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/Leino15a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/Leino15a
K. Rustan M. Leino:
Well-founded Functions and Extreme Predicates in Dafny: A Tutorial. IWIL@LPAR 2015: 52-66
[c80]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/Leino15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/Leino15
K. Rustan M. Leino:
Compiling Hilbert's epsilon operator. LPAR (short papers) 2015: 106-118
[c79]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/KoenigL16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/KoenigL16
Jason Koenig, K. Rustan M. Leino:
Programming Language Features for Refinement. Refine@FM 2015: 87-106
2014
[c78]
- view
  authority control:
- export record
  dblp key:
  - conf/fm/LeinoM14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fm/LeinoM14
K. Rustan M. Leino, Michal Moskal:
Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier. FM 2014: 382-398
[c77]
- view
  authority control:
- export record
  dblp key:
  - conf/fm/ChristakisLS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fm/ChristakisLS14
Maria Christakis, K. Rustan M. Leino, Wolfram Schulte:
Formalizing and Verifying a Modern Build Language. FM 2014: 643-657
[c76]
- view
  authority control:
- export record
  dblp key:
  - conf/tap/AminLR14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tap/AminLR14
Nada Amin, K. Rustan M. Leino, Tiark Rompf:
Computing with an SMT Solver. TAP@STAF 2014: 20-35
[c75]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/LeinoW14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/LeinoW14
K. Rustan M. Leino, Valentin Wüstholz:
The Dafny Integrated Development Environment. F-IDE 2014: 3-15
2013
[c74]
- view
  authority control:
- export record
  dblp key:
  - conf/icse/Leino04
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icse/Leino04
K. Rustan M. Leino:
Developing verified programs with dafny. ICSE 2013: 1488-1490
[c73]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Leino13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Leino13
K. Rustan M. Leino:
Automating Theorem Proving with SMT. ITP 2013: 2-16
[c72]
- view
  authority control:
- export record
  dblp key:
  - conf/vmcai/HeuleLMS13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vmcai/HeuleLMS13
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]
- view
  authority control:
- export record
  dblp key:
  - conf/vstte/LeinoP13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vstte/LeinoP13
K. Rustan M. Leino, Nadia Polikarpova:
Verified Calculations. VSTTE 2013: 170-190
2012
[c70]
- view
  authority control:
- export record
  dblp key:
  - conf/icse/CatanoLR12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icse/CatanoLR12
Néstor Cataño, K. Rustan M. Leino, Víctor Rivera:
The EventB2Dafny rodin plug-in. TOPI@ICSE 2012: 49-54
[c69]
- view
  authority control:
- export record
  dblp key:
  - conf/oopsla/Leino12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/oopsla/Leino12
K. Rustan M. Leino:
Staged program development. SPLASH 2012: 3-4
[c68]
- view
  authority control:
- export record
  dblp key:
  - conf/oopsla/LeinoM12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/oopsla/LeinoM12
K. Rustan M. Leino, Aleksandar Milicevic:
Program extrapolation with jennisys. OOPSLA 2012: 411-430
[c67]
- view
  authority control:
- export record
  dblp key:
  - conf/sigada/Leino12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sigada/Leino12
K. Rustan M. Leino:
Developing verified programs with Dafny. HILT 2012: 9-10
[c66]
- view
  authority control:
- export record
  dblp key:
  - conf/sigada/Leino12a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sigada/Leino12a
K. Rustan M. Leino:
Program proving using intermediate verification languages (IVLs) like boogie and why3. HILT 2012: 25-26
[c65]
- view
  authority control:
- export record
  dblp key:
  - conf/vmcai/Leino12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vmcai/Leino12
K. Rustan M. Leino:
Automating Induction with an SMT Solver. VMCAI 2012: 315-331
[c64]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/vstte/Leino12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vstte/Leino12
K. Rustan M. Leino:
Developing Verified Programs with Dafny. VSTTE 2012: 82
2011
[c63]
- view
  authority control:
- export record
  dblp key:
  - conf/ecoop/HeuleL0S11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ecoop/HeuleL0S11
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]
- view
  authority control:
- export record
  dblp key:
  - conf/fm/KlebanovMSLWAABCCHJLMPPRSTTUW11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fm/KlebanovMSLWAABCCHJLMPPRSTTUW11
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]
- view
  authority control:
- export record
  dblp key:
  - conf/laser/HerbertLQ11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/laser/HerbertLQ11
Luke Herbert, K. Rustan M. Leino, Jose Quaresma:
Using Dafny, an Automatic Program Verifier. LASER Summer School 2011: 156-181
[c60]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/nfm/Leino11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/nfm/Leino11
K. Rustan M. Leino:
From Retrospective Verification to Forward-Looking Development. NASA Formal Methods 2011: 1
[c59]
- view
  authority control:
- export record
  dblp key:
  - conf/sefm/GouesLM11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sefm/GouesLM11
Claire Le Goues, K. Rustan M. Leino, Michal Moskal:
The Boogie Verification Debugger (Tool Paper). SEFM 2011: 407-414
2010
[c58]
- view
  authority control:
- export record
  dblp key:
  - conf/birthday/Leino10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/birthday/Leino10
K. Rustan M. Leino:
Tools and Behavioral Abstraction: A Direction for Software Engineering. The Future of Software Engineering 2010: 115-124
[c57]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/esop/LeinoMS10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/esop/LeinoMS10
K. Rustan M. Leino, Peter Müller, Jan Smans:
Deadlock-Free Channels and Locks. ESOP 2010: 407-426
[c56]
- view
  authority control:
- export record
  dblp key:
  - conf/lpar/Leino10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/Leino10
K. Rustan M. Leino:
Dafny: An Automatic Program Verifier for Functional Correctness. LPAR (Dakar) 2010: 348-370
[c55]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/LeinoR10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/LeinoR10
K. Rustan M. Leino, Philipp Rümmer:
A Polymorphic Intermediate Verification Language: Design and Logical Encoding. TACAS 2010: 312-327
[c54]
- view
  authority control:
- export record
  dblp key:
  - conf/vmcai/Leino10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vmcai/Leino10
K. Rustan M. Leino:
Verifying Concurrent Programs with Chalice. VMCAI 2010: 2
[c53]
- view
  authority control:
- export record
  dblp key:
  - conf/vstte/LeinoM10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vstte/LeinoM10
K. Rustan M. Leino, Rosemary Monahan:
Dafny Meets the Verification Benchmarks Challenge. VSTTE 2010: 112-126
[c52]
- view
  authority control:
- export record
  dblp key:
  - conf/vstte/BarnettL10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vstte/BarnettL10
Michael Barnett, K. Rustan M. Leino:
To Goto Where No Statement Has Gone Before. VSTTE 2010: 157-168
2009
[c51]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/esop/LeinoM09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/esop/LeinoM09
K. Rustan M. Leino, Peter Müller:
A Basis for Verifying Multi-threaded Programs. ESOP 2009: 378-393
[c50]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/fase/LeinoM09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fase/LeinoM09
K. Rustan M. Leino, Ronald Middelkoop:
Proving Consistency of Pure Methods and Model Fields. FASE 2009: 231-245
[c49]
- view
  authority control:
- export record
  dblp key:
  - conf/fm/HoenickeLPSW09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fm/HoenickeLPSW09
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]
- view
  authority control:
- export record
  dblp key:
  - conf/fosad/LeinoMS09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fosad/LeinoMS09
K. Rustan M. Leino, Peter Müller, Jan Smans:
Verification of Concurrent Programs with Chalice. FOSAD 2009: 195-222
[c47]
- view
  authority control:
- export record
  dblp key:
  - conf/sac/LeinoM09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sac/LeinoM09
K. Rustan M. Leino, Rosemary Monahan:
Reasoning about comprehensions with first-order SMT solvers. SAC 2009: 615-622
2008
[c46]
- view
  authority control:
- export record
  dblp key:
  - conf/compsac/Leino08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/compsac/Leino08
K. Rustan M. Leino:
Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software Engineering. COMPSAC 2008: 11
[c45]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/esop/LeinoM08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/esop/LeinoM08
K. Rustan M. Leino, Peter Müller:
Verification of Equivalent-Results Methods. ESOP 2008: 307-321
[c44]
- view
  authority control:
- export record
  dblp key:
  - conf/indiaSE/LeinoW08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/indiaSE/LeinoW08
K. Rustan M. Leino, Angela Wallenburg:
Class-local object invariants. ISEC 2008: 57-66
[c43]
- view
  authority control:
- export record
  dblp key:
  - conf/laser/LeinoM08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/laser/LeinoM08
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]
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/BohmeLW08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/BohmeLW08
Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff:
HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier. TPHOLs 2008: 150-166
[c41]
- view
  authority control:
- export record
  dblp key:
  - conf/vstte/LeinoMW08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vstte/LeinoMW08
K. Rustan M. Leino, Peter Müller, Angela Wallenburg:
Flexible Immutability with Frozen Objects. VSTTE 2008: 192-208
2007
[c40]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/Leino07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/Leino07
K. Rustan M. Leino:
Designing Verification Conditions for Software. CADE 2007: 345
[c39]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/esop/LeinoS07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/esop/LeinoS07
K. Rustan M. Leino, Wolfram Schulte:
Using History Invariants to Verify Observers. ESOP 2007: 80-94
[c38]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/fase/DarvasL07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fase/DarvasL07
Ádám Darvas, K. Rustan M. Leino:
Practical Reasoning About Invocations and Implementations of Pure Methods. FASE 2007: 336-351
[c37]
- view
  authority control:
- export record
  dblp key:
  - conf/kbse/Leino07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/kbse/Leino07
K. Rustan M. Leino:
Specifying and verifying software. ASE 2007: 2
[c36]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/Leino07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/Leino07
K. Rustan M. Leino:
Verifying Object-Oriented Software: Lessons and Challenges. TACAS 2007: 2
2006
[c35]
- view
  authority control:
- export record
  dblp key:
  - conf/ershov/Leino06
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ershov/Leino06
K. Rustan M. Leino:
Specifying and Verifying Programs in Spec#. Ershov Memorial Conference 2006: 20
[c34]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/esop/LeinoM06
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/esop/LeinoM06
K. Rustan M. Leino, Peter Müller:
A Verification Methodology for Model Fields. ESOP 2006: 115-130
2005
[c33]
- view
  authority control:
- export record
  dblp key:
  - conf/aplas/LeinoL05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/aplas/LeinoL05
K. Rustan M. Leino, Francesco Logozzo:
Loop Invariants on Demand. APLAS 2005: 119-134
[c32]
- view
  - electronic edition @ univ-paris12.fr
  - no references & citations available
- export record
  dblp key:
  - conf/asm/Leino05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/asm/Leino05
K. Rustan M. Leino:
Program Verification and Programming Methodology. Abstract State Machines 2005: 73
[c31]
- view
  authority control:
- export record
  dblp key:
  - conf/fm/LeinoM05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fm/LeinoM05
K. Rustan M. Leino, Peter Müller:
Modular Verification of Static Class Invariants. FM 2005: 26-42
[c30]
- view
  authority control:
- export record
  dblp key:
  - conf/fmco/BarnettCDJL05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmco/BarnettCDJL05
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]
- view
  authority control:
- export record
  dblp key:
  - conf/paste/BarnettL05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/paste/BarnettL05
Michael Barnett, K. Rustan M. Leino:
Weakest-precondition of unstructured programs. PASTE 2005: 82-87
[c28]
- view
  authority control:
- export record
  dblp key:
  - conf/sefm/JacobsPLS05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sefm/JacobsPLS05
Bart Jacobs, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte:
Safe Concurrency for Aggregate Objects with Invariants. SEFM 2005: 137-147
[c27]
- view
  authority control:
- export record
  dblp key:
  - conf/sefm/Leino05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sefm/Leino05
K. Rustan M. Leino:
Invariants on Demand. SEFM 2005: 148-149
[c26]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/LeinoMO05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/LeinoMO05
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]
- view
  authority control:
- export record
  dblp key:
  - conf/vmcai/ChangL05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vmcai/ChangL05
Bor-Yuh Evan Chang, K. Rustan M. Leino:
Abstract Interpretation with Alien Expressions and Heap Structures. VMCAI 2005: 147-163
[c24]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/vstte/BarnettDFJLSV05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vstte/BarnettDFJLSV05
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]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/entcs/ChangRL05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/entcs/ChangRL05
Bor-Yuh Evan Chang, K. Rustan M. Leino:
Inferring Object Invariants: Extended Abstract. AIOOL@VMCAI 2005: 63-74
2004
[c22]
- view
  authority control:
- export record
  dblp key:
  - conf/cassis/BarnettLS04
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cassis/BarnettLS04
Mike Barnett, K. Rustan M. Leino, Wolfram Schulte:
The Spec# Programming System: An Overview. CASSIS 2004: 49-69
[c21]
- view
  authority control:
- export record
  dblp key:
  - conf/ecoop/LeinoM04
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ecoop/LeinoM04
K. Rustan M. Leino, Peter Müller:
Object Invariants in Dynamic Contexts. ECOOP 2004: 491-516
[c20]
- view
  authority control:
- export record
  dblp key:
  - conf/ictac/Leino04
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ictac/Leino04
K. Rustan M. Leino:
Challenges in Increasing Tool Support for Programming. ICTAC 2004: 35-35
[c19]
- view
  authority control:
- export record
  dblp key:
  - conf/sefm/LeinoS04
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sefm/LeinoS04
K. Rustan M. Leino, Wolfram Schulte:
Exception Safety for C#. SEFM 2004: 218-227
2003
[c18]
- view
  authority control:
- export record
  dblp key:
  - conf/birthday/AbadiL03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/birthday/AbadiL03
Martín Abadi, K. Rustan M. Leino:
A Logic of Object-Oriented Programs. Verification: Theory and Practice 2003: 11-41
[c17]
- view
  authority control:
- export record
  dblp key:
  - conf/oopsla/FahndrichL03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/oopsla/FahndrichL03
Manuel Fähndrich, K. Rustan M. Leino:
Declaring and checking non-null types in an object-oriented language. OOPSLA 2003: 302-312
[c16]
- view
  authority control:
- export record
  dblp key:
  - conf/spin/Leino03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/spin/Leino03
K. Rustan M. Leino:
A SAT Characterization of Boolean-Program Correctness. SPIN 2003: 104-120
[c15]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/entcs/BurdyCCEKLLP03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/entcs/BurdyCCEKLLP03
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
[c14]
- view
  authority control:
- export record
  dblp key:
  - conf/pldi/FlanaganLLNSS02
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pldi/FlanaganLLNSS02
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]
- view
  authority control:
- export record
  dblp key:
  - conf/pldi/LeinoPZ02
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pldi/LeinoPZ02
K. Rustan M. Leino, Arnd Poetzsch-Heffter, Yunhong Zhou:
Using Data Groups to Specify and Check Side Effects. PLDI 2002: 246-257
2001
[c12]
- view
  authority control:
- export record
  dblp key:
  - conf/dagstuhl/Leino01
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/dagstuhl/Leino01
K. Rustan M. Leino:
Extended Static Checking: A Ten-Year Perspective. Informatics 2001: 157-175
[c11]
- view
  authority control:
- export record
  dblp key:
  - conf/fm/FlanaganL01
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fm/FlanaganL01
Cormac Flanagan, K. Rustan M. Leino:
Houdini, an Annotation Assistant for ESC/Java. FME 2001: 500-517
[c10]
- view
  authority control:
- export record
  dblp key:
  - conf/sas/Leino01
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sas/Leino01
K. Rustan M. Leino:
Applications of Extended Static Checking. SAS 2001: 185-193
2000
[c9]
- view
  authority control:
- export record
  dblp key:
  - conf/oopsla/LeavensRLPJ00
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/oopsla/LeavensRLPJ00
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
1999
[c8]
- no documents available
  - no references & citations available
- export record
  dblp key:
  - conf/ecoopw/LeinoSS99
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ecoopw/LeinoSS99
K. Rustan M. Leino, James B. Saxe, Raymie Stata:
Checking Java Programs via Guarded Commands. ECOOP Workshops 1999: 110-111
1998
[c7]
- view
  authority control:
- export record
  dblp key:
  - conf/cc/LeinoN98
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cc/LeinoN98
K. Rustan M. Leino, Greg Nelson:
An Extended Static Checker for Modular-3. CC 1998: 302-305
[c6]
- view
  authority control:
- export record
  dblp key:
  - conf/esop/Leino98
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/esop/Leino98
K. Rustan M. Leino:
Recursive Object Types in a Logic of Object-Oriented Programs. ESOP 1998: 170-184
[c5]
- view
  authority control:
- export record
  dblp key:
  - conf/mpc/LeinoJ98
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/mpc/LeinoJ98
K. Rustan M. Leino, Rajeev Joshi:
A Semantic Approach to Secure Information Flow. MPC 1998: 254-271
[c4]
- view
  authority control:
- export record
  dblp key:
  - conf/oopsla/Leino98
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/oopsla/Leino98
K. Rustan M. Leino:
Data Groups: Specifying the Modification of Extended State. OOPSLA 1998: 144-153
[c3]
- no documents available
  - no references & citations available
- export record
  dblp key:
  - conf/procomet/Leino98
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/procomet/Leino98
K. Rustan M. Leino:
Extended static checking. PROCOMET 1998: 1-2
1997
[c2]
- view
  authority control:
- export record
  dblp key:
  - conf/tapsoft/AbadiL97
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tapsoft/AbadiL97
Martín Abadi, K. Rustan M. Leino:
A Logic of Object-Oriented Programs. TAPSOFT 1997: 682-696
1994
[c1]
- no documents available
  - no references & citations available
- export record
  dblp key:
  - conf/procomet/LeinoS94
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/procomet/LeinoS94
K. Rustan M. Leino, Jan L. A. van de Snepscheut:
Semantics of Exceptions. PROCOMET 1994: 447-466

Parts in Books or Collections

see FAQ

What is the meaning of the colors in the publication lists?

2012
[p1]
- view
  authority control:
- export record
  dblp key:
  - series/natosec/KoenigL12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/series/natosec/KoenigL12
Jason Koenig, K. Rustan M. Leino:
Getting Started with Dafny: A Guide. Software Safety and Security 2012: 152-181

Editorship

see FAQ

What is the meaning of the colors in the publication lists?

2021
[e4]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/2021-1
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/2021-1
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]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/2021-2
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/2021-2
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]
2016
[e2]
- view
  authority control:
- export record
  dblp key:
  - conf/vmcai/2016
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vmcai/2016
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]
2011
[e1]
- view
  authority control:
- export record
  dblp key:
  - conf/tacas/2011
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/2011
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]

Informal and Other Publications

see FAQ

What is the meaning of the colors in the publication lists?

2004
[i1]
- view
  - electronic edition @ arxiv.org (open access)
  - references & citations
- export record
  dblp key:
  - journals/corr/cs-PL-0408045
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/cs-PL-0408045
Viktor Kuncak, K. Rustan M. Leino:
On computing the fixpoint of a set of boolean equations. CoRR cs.PL/0408045 (2004)

Coauthor Index

see FAQ

a service of

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.