K. Rustan M. Leino
#167,049
Most Influential Person Now
Ph.D. California Institute of Technology 1995
K. Rustan M. Leino's Degrees
- PhD Computer Science California Institute of Technology
Similar Degrees You Can Earn
Why Is K. Rustan M. Leino Influential?
(Suggest an Edit or Addition)K. Rustan M. Leino's Published Works
Number of citations in a given year to any of this author's works
Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author
Published Works
- The Spec# Programming System: An Overview (2004) (1196)
- Boogie: A Modular Reusable Verifier for Object-Oriented Programs (2005) (952)
- An overview of JML tools and applications (2003) (923)
- Dafny: An Automatic Program Verifier for Functional Correctness (2010) (914)
- Extended static checking (1998) (508)
- Houdini, an Annotation Assistant for ESC/Java (2001) (434)
- Verification of Object-Oriented Programs with Invariants (2003) (374)
- Weakest-precondition of unstructured programs (2005) (255)
- Object Invariants in Dynamic Contexts (2004) (249)
- Declaring and checking non-null types in an object-oriented language (2003) (211)
- A semantic approach to secure information flow (2000) (188)
- Data groups: specifying the modification of extended state (1998) (187)
- A Logic of Object-Oriented Programs (1997) (184)
- Efficient weakest preconditions (2005) (169)
- BoogiePL: A typed procedural language for checking object-oriented programs (2005) (168)
- Behavioral interface specification languages (2012) (168)
- A Basis for Verifying Multi-threaded Programs (2009) (164)
- Data abstraction and information hiding (2002) (157)
- Towards Reliable Modular Programs (1995) (156)
- Tools and Algorithms for the Construction and Analysis of Systems (1996) (150)
- Specification and verification challenges for sequential object-oriented programs (2007) (145)
- ESC/Java User's Manual (2000) (134)
- Using data groups to specify and check side effects (2002) (133)
- Specification and verification (2011) (131)
- Verification of Concurrent Programs with Chalice (2009) (128)
- This is Boogie 2 (2016) (121)
- Checking Java Programs via Guarded Commands (1999) (113)
- A programming model for concurrent object-oriented programs (2008) (106)
- Vale: Verifying High-Performance Cryptographic Assembly Code (2017) (104)
- A Polymorphic Intermediate Verification Language: Design and Logical Encoding (2010) (98)
- The 1st Verified Software Competition: Experience Report (2011) (92)
- The Spec# Programming System: Challenges and Directions (2005) (91)
- A Verification Methodology for Model Fields (2006) (88)
- Safe concurrency for aggregate objects with invariants (2005) (86)
- Loop Invariants on Demand (2005) (82)
- Automating Induction with an SMT Solver (2012) (82)
- An Extended Static Checker for Modular-3 (1998) (81)
- JML (poster session): notations and tools supporting detailed design in Java (2000) (78)
- Developing verified programs with Dafny (2012) (74)
- Abstract Interpretation with Alien Expressions and Heap Structures (2005) (73)
- Extended Static Checking: A Ten-Year Perspective (2001) (70)
- Generating error traces from verification-condition counterexamples (2005) (65)
- Practical Reasoning About Invocations and Implementations of Pure Methods (2007) (65)
- Modular Verification of Static Class Invariants (2005) (62)
- Deadlock-Free Channels and Locks (2010) (62)
- The Dafny Integrated Development Environment (2014) (60)
- Annotation inference for modular checkers (2001) (54)
- Recursive Object Types in a Logic of Object-Oriented Programs (1998) (53)
- Using History Invariants to Verify Observers (2007) (52)
- Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs (2008) (52)
- Reasoning about comprehensions with first-order SMT solvers (2009) (51)
- The Boogie Verification Debugger (Tool Paper) (2011) (50)
- Heap Monotonic Typestate (2003) (44)
- Finding stale‐value errors in concurrent programs (2004) (44)
- Trigger Selection Strategies to Stabilize Program Verifiers (2016) (41)
- Flexible Immutability with Frozen Objects (2008) (39)
- Dafny Meets the Verification Benchmarks Challenge (2010) (39)
- Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier (2014) (38)
- Abstract Read Permissions: Fractional Permissions without the Fractions (2013) (37)
- Exception safety for C# (2004) (32)
- HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier (2008) (32)
- Accessible Software Verification with Dafny (2017) (32)
- Verification of Equivalent-Results Methods (2008) (31)
- The boogie verification debugger (2011) (31)
- Verified Calculations (2013) (30)
- Specification and Verification of Object-Oriented Software (2016) (28)
- Program extrapolation with jennisys (2012) (27)
- Fine-Grained Caching of Verification Results (2015) (26)
- The Spec# Programming System (2012) (26)
- PLDI 2002: Extended static checking for Java (2013) (24)
- It's Doomed; We Can Prove It (2009) (24)
- Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domain (2007) (24)
- Integrated Environment for Diagnosing Verification Errors (2016) (23)
- Virginity: A Contribution to the Specification of Object-Oriented Software (1999) (23)
- Formalizing and Verifying a Modern Build Language (2014) (23)
- Semantics of Exceptions (1994) (20)
- A Verifying Compiler for a Multi-threaded Object-Oriented Language (2007) (20)
- Proving Consistency of Pure Methods and Model Fields (2009) (19)
- Ecstatic: An object-oriented programming language with an axiomatic semantics (2006) (19)
- Computing with an SMT Solver (2014) (19)
- Doomed program points (2010) (19)
- Joining Specification Statements (1999) (18)
- Getting Started with Dafny: A Guide (2012) (18)
- Verification Condition Splitting (2008) (17)
- Automatic verification of textbook programs that usecomprehensions (2007) (17)
- A SAT Characterization of Boolean-Program Correctness (2003) (16)
- Class-local object invariants (2008) (15)
- Fractional permissions without the fractions (2011) (14)
- Using Dafny, an Automatic Program Verifier (2011) (14)
- Fractional permissions without the fractions (2011) (14)
- Modular verification of global module invariants in object-oriented programs (2004) (13)
- Automating Theorem Proving with SMT (2013) (13)
- Stepwise refinement of heap-manipulating code in Chalice (2012) (12)
- A myth in the modular specification of programs (1996) (11)
- Specifying and Verifying Programs in Spec# (2006) (11)
- The EventB2Dafny Rodin plug-in (2012) (11)
- Automatic Verification of Textbook Programs That Use (2007) (10)
- Programming Language Features for Refinement (2015) (10)
- Applications of Extended Static Checking (2001) (10)
- Verification, Model Checking, and Abstract Interpretation (2016) (9)
- Developing verified programs with Dafny (2012) (9)
- Non-null types in an object-oriented language (2002) (9)
- A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover (2005) (9)
- Verifying Concurrent Programs with Chalice (2010) (9)
- Inferring Object Invariants: Extended Abstract (2005) (8)
- Specifying and verifying software (2007) (7)
- Automatic verification of Dafny programs with traits (2015) (6)
- Program proving using intermediate verification languages (IVLs) like boogie and why3 (2012) (6)
- Safe Concurrency for Aggregate Objects with Invariants: Soundness Proof (2005) (6)
- Proceedings of the 17th international conference on Tools and algorithms for the construction and analysis of systems: part of the joint European conferences on theory and practice of software (2011) (5)
- Tools and Behavioral Abstraction: A Direction for Software Engineering (2010) (4)
- On computing the fixpoint of a set of boolean equations (2003) (4)
- Modeling Concurrency in Dafny (2017) (4)
- To Goto Where No Statement Has Gone Before (2010) (4)
- An Assertional Proof of the Stability and Correctness of Natural Mergesort (2015) (4)
- Theory and Use of Conditional Composition (1994) (3)
- The 1st Verified Software Competition, Extended Experience Report (2011) (3)
- Extensions to an Object Oriented Programming Language for Programming Fine-grain Multicomputers (1992) (3)
- Learning to do program verification (2010) (3)
- Designing Verification Conditions for Software (2007) (2)
- Modular Verification Scopes via Export Sets and Translucent Exports (2018) (2)
- Multicomputer Programming with Modula-3D (1993) (2)
- Specifying the modification of extended state (1997) (2)
- Automatic verification of textbook programs (2007) (2)
- Invariants on Demand (2005) (2)
- Constructing a Program with Exceptions (1995) (2)
- Deadlock-free Channels and Locks (extended version) (2010) (2)
- Real estate of names (2001) (2)
- Finding stale-value errors in concurrent programs: Research Articles (2004) (2)
- Verification, Model Checking, and Abstract Interpretation : 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings (2016) (2)
- Automated Stepwise Refinement of Heap-Manipulating Code Manuscript KRML 211 – October 9 , 2010 (2010) (2)
- Tools for software verification (2013) (2)
- Staged program development (2012) (2)
- Well-founded Functions and Extreme Predicates in Dafny: A Tutorial (2016) (2)
- Quicksort Revisited - Verifying Alternative Versions of Quicksort (2016) (2)
- Verified Software: Theories, Tools, and Experiments, VSTTE 2006, Workshop proceedings (2006) (1)
- A method for showing progress (1995) (1)
- Verifying Object-Oriented Software: Lessons and Challenges (2007) (1)
- Conditional composition (2005) (1)
- The Boogie 2 Type System : Design and Verification Condition Generation (2009) (1)
- Compiling Hilbert's epsilon operator (2015) (1)
- Abstraction dependencies (2003) (1)
- A small dual-automorphic lattice with no involutory dual automorphism (1997) (0)
- Challenges in Increasing Tool Support for Programming (2004) (0)
- Trigger Selection Strategies to Stabilize Program (2016) (0)
- From Retrospective Verification to Forward-Looking Development (2011) (0)
- Co-induction in an Auto-Active Program (2013) (0)
- Program Verification and Programming Methodology (2005) (0)
- Stepwise refinement of heap-manipulating code in Chalice (2012) (0)
- Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 9583 (2016) (0)
- Heap Monotonic Typestates (Extended Abstract) (2003) (0)
- Using Dafny for programs and proof (2014) (0)
- Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software Engineering (2008) (0)
- Computing Permutation Encodings (1999) (0)
- Verifying Invariants in Object-Oriented Programs (2017) (0)
- Reasoning about Comprehensions withFirst-OrderSMT Solvers (2009) (0)
- Specifying the boundary between unverified and verified code (2022) (0)
- Tools for software verification (2013) (0)
- Specifying the Boundary Between Unverified and Verified Code (2022) (0)
- Read-only by specification (2008) (0)
- Snakes, Birds, and Swords : Metaphors in the Graphic Novel Epileptic by David B. (2016) (0)
- Verification of Concurrent Object-Oriented Programs (2016) (0)
- Technologies for finding errors in object-oriented software (2017) (0)
- A Foundation for Verifying Concurrent Programs (Lecture 1) (2017) (0)
This paper list is powered by the following services:
What Schools Are Affiliated With K. Rustan M. Leino?
K. Rustan M. Leino is affiliated with the following schools:
