K. Rustan M. Leino

According to our database1, K. Rustan M. Leino authored at least 111 papers between 1994 and 2018.

Collaborative distances:

Awards

ACM Fellow

ACM Fellow 2016, "For contributions to making program verification accessible and practical".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2018
Modular Verification Scopes via Export Sets and Translucent Exports.
Proceedings of the Principled Software Development, 2018

2017
Accessible Software Verification with Dafny.
IEEE Softw., 2017

Vale: Verifying High-Performance Cryptographic Assembly Code.
Proceedings of the 26th USENIX Security Symposium, 2017

Modeling Concurrency in Dafny.
Proceedings of the Engineering Trustworthy Software Systems - Third International School, 2017

2016
Integrated Environment for Diagnosing Verification Errors.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Trigger Selection Strategies to Stabilize Program Verifiers.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Quicksort Revisited - Verifying Alternative Versions of Quicksort.
Proceedings of the Theory and Practice of Formal Methods, 2016

2015
An Assertional Proof of the Stability and Correctness of Natural Mergesort.
ACM Trans. Comput. Log., 2015

Programming Language Features for Refinement.
Proceedings of the Proceedings 17th International Workshop on Refinement, 2015

Compiling Hilbert's epsilon operator.
Proceedings of the 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, 2015

Automatic verification of Dafny programs with traits.
Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, 2015

Fine-Grained Caching of Verification Results.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014
The Dafny Integrated Development Environment.
Proceedings of the Proceedings 1st Workshop on Formal Integrated Development Environment, 2014

Computing with an SMT Solver.
Proceedings of the Tests and Proofs - 8th International Conference, 2014

Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier.
Proceedings of the FM 2014: Formal Methods, 2014

Formalizing and Verifying a Modern Build Language.
Proceedings of the FM 2014: Formal Methods, 2014

2013
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., 2013

PLDI 2002: Extended static checking for Java.
ACM SIGPLAN Notices, 2013

Verified Calculations.
Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Abstract Read Permissions: Fractional Permissions without the Fractions.
Proceedings of the Verification, 2013

Automating Theorem Proving with SMT.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012
Getting Started with Dafny: A Guide.
Proceedings of the Software Safety and Security - Tools for Analysis and Verification, 2012

Stepwise refinement of heap-manipulating code in Chalice.
Formal Aspects Comput., 2012

Behavioral interface specification languages.
ACM Comput. Surv., 2012

Developing Verified Programs with Dafny.
Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

Automating Induction with an SMT Solver.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

Program proving using intermediate verification languages (IVLs) like boogie and why3.
Proceedings of the 2012 ACM Conference on High Integrity Language Technology, 2012

Program extrapolation with jennisys.
Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

Staged program development.
Proceedings of the Conference on Systems, 2012

The EventB2Dafny rodin plug-in.
Proceedings of the Second International Workshop on Developing Tools as Plug-Ins, 2012

2011
Specification and verification: the Spec# experience.
Commun. ACM, 2011

The Boogie Verification Debugger (Tool Paper).
Proceedings of the Software Engineering and Formal Methods - 9th International Conference, 2011

From Retrospective Verification to Forward-Looking Development.
Proceedings of the NASA Formal Methods, 2011

Using Dafny, an Automatic Program Verifier.
Proceedings of the Tools for Practical Software Verification, 2011


Fractional permissions without the fractions.
Proceedings of the 13th Workshop on Formal Techniques for Java-Like Programs, 2011

2010
Doomed program points.
Formal Methods Syst. Des., 2010

Learning to do program verification.
Commun. ACM, 2010

Dafny Meets the Verification Benchmarks Challenge.
Proceedings of the Verified Software: Theories, 2010

To Goto Where No Statement Has Gone Before.
Proceedings of the Verified Software: Theories, 2010

Verifying Concurrent Programs with Chalice.
Proceedings of the Verification, 2010

A Polymorphic Intermediate Verification Language: Design and Logical Encoding.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Dafny: An Automatic Program Verifier for Functional Correctness.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Deadlock-Free Channels and Locks.
Proceedings of the Programming Languages and Systems, 2010

Tools and Behavioral Abstraction: A Direction for Software Engineering.
Proceedings of the Future of Software Engineering., 2010

2009
Reasoning about comprehensions with first-order SMT solvers.
Proceedings of the 2009 ACM Symposium on Applied Computing (SAC), 2009

Verification of Concurrent Programs with Chalice.
Proceedings of the Foundations of Security Analysis and Design V, 2009

It's Doomed; We Can Prove It.
Proceedings of the FM 2009: Formal Methods, 2009

Proving Consistency of Pure Methods and Model Fields.
Proceedings of the Fundamental Approaches to Software Engineering, 2009

A Basis for Verifying Multi-threaded Programs.
Proceedings of the Programming Languages and Systems, 2009

2008
A programming model for concurrent object-oriented programs.
ACM Trans. Program. Lang. Syst., 2008

Flexible Immutability with Frozen Objects.
Proceedings of the Verified Software: Theories, 2008

HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier.
Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs.
Proceedings of the Advanced Lectures on Software Engineering, 2008

Class-local object invariants.
Proceedings of the Proceeding of the 1st Annual India Software Engineering Conference, 2008

Verification of Equivalent-Results Methods.
Proceedings of the Programming Languages and Systems, 2008

Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software Engineering.
Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference, 2008

2007
Specification and verification challenges for sequential object-oriented programs.
Formal Aspects Comput., 2007

Verifying Object-Oriented Software: Lessons and Challenges.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Specifying and verifying software.
Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007), 2007

Practical Reasoning About Invocations and Implementations of Pure Methods.
Proceedings of the Fundamental Approaches to Software Engineering, 2007

Using History Invariants to Verify Observers.
Proceedings of the Programming Languages and Systems, 2007

Designing Verification Conditions for Software.
Proceedings of the Automated Deduction, 2007

2006
A Verification Methodology for Model Fields.
Proceedings of the Programming Languages and Systems, 2006

Specifying and Verifying Programs in Spec#.
Proceedings of the Perspectives of Systems Informatics, 2006

2005
Generating error traces from verification-condition counterexamples.
Sci. Comput. Program., 2005

Efficient weakest preconditions.
Inf. Process. Lett., 2005

Inferring Object Invariants: Extended Abstract.
Electron. Notes Theor. Comput. Sci., 2005

The Spec# Programming System: Challenges and Directions.
Proceedings of the Verified Software: Theories, 2005

Abstract Interpretation with Alien Expressions and Heap Structures.
Proceedings of the Verification, 2005

A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Invariants on Demand.
Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 2005

Safe Concurrency for Aggregate Objects with Invariants.
Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 2005

Weakest-precondition of unstructured programs.
Proceedings of the 2005 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, 2005

Boogie: A Modular Reusable Verifier for Object-Oriented Programs.
Proceedings of the Formal Methods for Components and Objects, 4th International Symposium, 2005

Modular Verification of Static Class Invariants.
Proceedings of the FM 2005: Formal Methods, 2005

Program Verification and Programming Methodology.
Proceedings of the 12th International Workshop on Abstract State Machines, 2005

Loop Invariants on Demand.
Proceedings of the Programming Languages and Systems, Third Asian Symposium, 2005

2004
Verification of Object-Oriented Programs with Invariants.
J. Object Technol., 2004

On computing the fixpoint of a set of boolean equations
CoRR, 2004

Finding stale-value errors in concurrent programs.
Concurr. Pract. Exp., 2004

Exception Safety for C#.
Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004

Challenges in Increasing Tool Support for Programming.
Proceedings of the Theoretical Aspects of Computing, 2004

Object Invariants in Dynamic Contexts.
Proceedings of the ECOOP 2004, 2004

The Spec# Programming System: An Overview.
Proceedings of the Construction and Analysis of Safe, 2004

2003
An overview of JML tools and applications.
Electron. Notes Theor. Comput. Sci., 2003

A SAT Characterization of Boolean-Program Correctness.
Proceedings of the Model Checking Software, 2003

Declaring and checking non-null types in an object-oriented language.
Proceedings of the 2003 ACM SIGPLAN Conference on Object-Oriented Programming Systems, 2003

2002
Data abstraction and information hiding.
ACM Trans. Program. Lang. Syst., 2002

Using Data Groups to Specify and Check Side Effects.
Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2002

Extended Static Checking for Java.
Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2002

2001
Real estate of names.
Inf. Process. Lett., 2001

Annotation inference for modular checkers.
Inf. Process. Lett., 2001

Applications of Extended Static Checking.
Proceedings of the Static Analysis, 8th International Symposium, 2001

Houdini, an Annotation Assistant for ESC/Java.
Proceedings of the FME 2001: Formal Methods for Increasing Software Productivity, 2001

Extended Static Checking: A Ten-Year Perspective.
Proceedings of the Informatics - 10 Years Back. 10 Years Ahead., 2001

2000
A semantic approach to secure information flow.
Sci. Comput. Program., 2000

JML (poster session): notations and tools supporting detailed design in Java.
Proceedings of the Object Oriented Programming Systems Languages and Applications Conference, 2000

1999
Joining Specification Statements.
Theor. Comput. Sci., 1999

Virginity: A Contribution to the Specification of Object-Oriented Software.
Inf. Process. Lett., 1999

Computing Permutation Encodings.
Formal Aspects Comput., 1999

Checking Java Programs via Guarded Commands.
Proceedings of the Object-Oriented Technology, ECOOP'99 Workshop Reader, 1999

1998
Recursive Object Types in a Logic of Object-Oriented Programs.
Nord. J. Comput., 1998

Extended static checking.
Proceedings of the Programming Concepts and Methods, 1998

Data Groups: Specifying the Modification of Extended State.
Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, 1998

An Extended Static Checker for Modular-3.
Proceedings of the Compiler Construction, 7th International Conference, 1998

1997
A Logic of Object-Oriented Programs.
Proceedings of the TAPSOFT'97: Theory and Practice of Software Development, 1997

1995
Constructing a Program with Exceptions.
Inf. Process. Lett., 1995

Conditional Composition.
Formal Aspects Comput., 1995

A Method for Showing Progress.
Formal Aspects Comput., 1995

1994
Semantics of Exceptions.
Proceedings of the Programming Concepts, 1994


  Loading...