BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × Canada
1 × China
1 × Hungary
1 × Ireland
1 × Italy
1 × Norway
1 × Singapore
1 × Spain
1 × The Netherlands
1 × Uruguay
2 × Cyprus
2 × France
4 × Germany
5 × United Kingdom
6 × Portugal
8 × USA
Collaborated with:
∅ P.Müller W.Schulte M.Moskal C.Flanagan G.Nelson V.Wüstholz R.Monahan A.Milicevic P.Rümmer R.Middelkoop Á.Darvas M.Barnett B.E.Chang M.Fähndrich M.Abadi C.Pit-Claudel J.Smans M.Christakis N.Amin T.Rompf C.L.Goues M.Musuvathi X.Ou A.Poetzsch-Heffter Y.Zhou B.Jacobs F.Piessens S.Heule A.J.Summers J.Hoenicke A.Podelski M.Schäf T.Wies M.Lillibridge J.B.Saxe R.Stata V.Klebanov N.Shankar G.T.Leavens E.Alkassar R.Arthan D.Bronish R.Chapman E.Cohen M.A.Hillebrand N.Polikarpova T.Ridge S.Tobies T.Tuerk M.Ulbrich B.Weiß
Talks about:
program (11) verifi (11) verif (8) object (7) invari (5) softwar (4) languag (4) static (4) orient (4) extend (4)

Person: K. Rustan M. Leino

DBLP DBLP: Leino:K=_Rustan_M=

Facilitated 1 volumes:

TACAS 2011Ed

Contributed to:

CAV 20152015
FM 20142014
TAP 20142014
ICSE 20132013
VMCAI 20132013
HILT 20122012
OOPSLA 20122012
VMCAI 20122012
FM 20112011
SEFM 20112011
ESOP 20102010
TACAS 20102010
VMCAI 20102010
ESOP 20092009
FASE 20092009
FM 20092009
SAC 20092009
ESOP 20082008
ASE 20072007
CADE 20072007
ESOP 20072007
FASE 20072007
TACAS 20072007
ESOP 20062006
FM 20052005
PASTE 20052005
SEFM 20052005
TACAS 20052005
VMCAI 20052005
ECOOP 20042004
SEFM 20042004
OOPSLA 20032003
PLDI 20022002
FME 20012001
SAS 20012001
CC 19981998
ESOP 19981998
OOPSLA 19981998
TAPSOFT CAAP/FASE 19971997
CAV (1) 20162016

Wrote 44 papers:

CAV-2015-LeinoW #fine-grained #verification
Fine-Grained Caching of Verification Results (KRML, VW), pp. 380–397.
FM-2014-ChristakisLS #formal method #verification
Formalizing and Verifying a Modern Build Language (MC, KRML, WS), pp. 643–657.
FM-2014-LeinoM #automation #induction #proving #verification
Co-induction Simply — Automatic Co-inductive Proofs in a Program Verifier (KRML, MM), pp. 382–398.
TAP-2014-AminLR #smt
Computing with an SMT Solver (NA, KRML, TR), pp. 20–35.
ICSE-2013-Leino #source code
Developing verified programs with dafny (KRML), pp. 1488–1490.
VMCAI-2013-HeuleLMS
Abstract Read Permissions: Fractional Permissions without the Fractions (SH, KRML, PM, AJS), pp. 315–334.
HILT-2012-Leino #source code
Developing verified programs with Dafny (KRML), pp. 9–10.
HILT-2012-Leino12a #proving #using #verification #why
Program proving using intermediate verification languages (IVLs) like boogie and why3 (KRML), pp. 25–26.
OOPSLA-2012-LeinoM
Program extrapolation with jennisys (KRML, AM), pp. 411–430.
VMCAI-2012-Leino #automation #induction #smt
Automating Induction with an SMT Solver (KRML), pp. 315–331.
FM-2011-KlebanovMSLWAABCCHJLMPPRSTTUW #case study #contest #experience
The 1st Verified Software Competition: Experience Report (VK, PM, NS, GTL, VW, EA, RA, DB, RC, EC, MAH, BJ, KRML, RM, FP, NP, TR, JS, ST, TT, MU, BW), pp. 154–168.
SEFM-2011-GouesLM #debugging #verification
The Boogie Verification Debugger (CLG, KRML, MM), pp. 407–414.
ESOP-2010-LeinoMS #concurrent
Deadlock-Free Channels and Locks (KRML, PM, JS), pp. 407–426.
TACAS-2010-LeinoR #design #encoding #logic #polymorphism #verification
A Polymorphic Intermediate Verification Language: Design and Logical Encoding (KRML, PR), pp. 312–327.
VMCAI-2010-Leino #concurrent #source code #verification
Verifying Concurrent Programs with Chalice (KRML), p. 2.
ESOP-2009-LeinoM #concurrent #multi #source code #thread #verification
A Basis for Verifying Multi-threaded Programs (KRML, PM), pp. 378–393.
FASE-2009-LeinoM #consistency #proving
Proving Consistency of Pure Methods and Model Fields (KRML, RM), pp. 231–245.
FM-2009-HoenickeLPSW
It’s Doomed; We Can Prove It (JH, KRML, AP, MS, TW), pp. 338–353.
SAC-2009-LeinoM #first-order #reasoning #smt
Reasoning about comprehensions with first-order SMT solvers (KRML, RM), pp. 615–622.
ESOP-2008-LeinoM #verification
Verification of Equivalent-Results Methods (KRML, PM), pp. 307–321.
ASE-2007-Leino #specification #verification
Specifying and verifying software (KRML), p. 2.
CADE-2007-Leino #design #verification
Designing Verification Conditions for Software (KRML), p. 345.
ESOP-2007-LeinoS #invariant #using #verification
Using History Invariants to Verify Observers (KRML, WS), pp. 80–94.
FASE-2007-DarvasL #implementation #reasoning
Practical Reasoning About Invocations and Implementations of Pure Methods (ÁD, KRML), pp. 336–351.
TACAS-2007-Leino #challenge #object-oriented #verification
Verifying Object-Oriented Software: Lessons and Challenges (KRML), p. 2.
ESOP-2006-LeinoM #verification
A Verification Methodology for Model Fields (KRML, PM), pp. 115–130.
FM-2005-LeinoM #composition #invariant #verification
Modular Verification of Static Class Invariants (KRML, PM), pp. 26–42.
PASTE-2005-BarnettL #source code
Weakest-precondition of unstructured programs (MB, KRML), pp. 82–87.
SEFM-2005-JacobsPLS #concurrent #invariant
Safe Concurrency for Aggregate Objects with Invariants (BJ, FP, KRML, WS), pp. 137–147.
SEFM-2005-Leino #invariant
Invariants on Demand (KRML), pp. 148–149.
TACAS-2005-LeinoMO #proving #quantifier #theorem proving
A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover (KRML, MM, XO), pp. 334–348.
VMCAI-2005-ChangL #abstract interpretation
Abstract Interpretation with Alien Expressions and Heap Structures (BYEC, KRML), pp. 147–163.
ECOOP-2004-LeinoM #invariant
Object Invariants in Dynamic Contexts (KRML, PM), pp. 491–516.
SEFM-2004-LeinoS #c# #exception #safety
Exception Safety for C# (KRML, WS), pp. 218–227.
OOPSLA-2003-FahndrichL #object-oriented
Declaring and checking non-null types in an object-oriented language (MF, KRML), pp. 302–312.
PLDI-2002-FlanaganLLNSS #java #static analysis
Extended Static Checking for Java (CF, KRML, ML, GN, JBS, RS), pp. 234–245.
PLDI-2002-LeinoPZ #using
Using Data Groups to Specify and Check Side Effects (KRML, APH, YZ), pp. 246–257.
FME-2001-FlanaganL #java
Houdini, an Annotation Assistant for ESC/Java (CF, KRML), pp. 500–517.
SAS-2001-Leino #static analysis
Applications of Extended Static Checking (KRML), pp. 185–193.
CC-1998-LeinoN #static analysis
An Extended Static Checker for Modular-3 (KRML, GN), pp. 302–305.
ESOP-1998-Leino #logic #object-oriented #recursion #source code
Recursive Object Types in a Logic of Object-Oriented Programs (KRML), pp. 170–184.
OOPSLA-1998-Leino #specification
Data Groups: Specifying the Modification of Extended State (KRML), pp. 144–153.
TAPSOFT-1997-AbadiL #logic #object-oriented #source code
A Logic of Object-Oriented Programs (MA, KRML), pp. 682–696.
CAV-2016-LeinoP #verification
Trigger Selection Strategies to Stabilize Program Verifiers (KRML, CPC), pp. 361–381.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.