Search the dblp DataBase
K. Rustan M. Leino :
[Publications ]
[Author Rank by year ]
[Co-authors ]
[Prefers ]
[Cites ]
[Cited by ]
Publications of Author
K. Rustan M. Leino , Francesco Logozzo Loop Invariants on Demand. [Citation Graph (0, 0)][DBLP ] APLAS, 2005, pp:119-134 [Conf ] Martín Abadi , K. Rustan M. Leino A Logic of Object-Oriented Programs. [Citation Graph (0, 0)][DBLP ] Verification: Theory and Practice, 2003, pp:11-41 [Conf ] K. Rustan M. Leino , Greg Nelson An Extended Static Checker for Modular-3. [Citation Graph (0, 0)][DBLP ] CC, 1998, pp:302-305 [Conf ] K. Rustan M. Leino Extended Static Checking: A Ten-Year Perspective. [Citation Graph (0, 0)][DBLP ] Informatics, 2001, pp:157-175 [Conf ] K. Rustan M. Leino , Peter Müller Object Invariants in Dynamic Contexts. [Citation Graph (0, 0)][DBLP ] ECOOP, 2004, pp:491-516 [Conf ] K. Rustan M. Leino , James B. Saxe , Raymie Stata Checking Java Programs via Guarded Commands. [Citation Graph (0, 0)][DBLP ] ECOOP Workshops, 1999, pp:110-111 [Conf ] K. Rustan M. Leino Recursive Object Types in a Logic of Object-Oriented Programs. [Citation Graph (0, 0)][DBLP ] ESOP, 1998, pp:170-184 [Conf ] K. Rustan M. Leino , Peter Müller A Verification Methodology for Model Fields. [Citation Graph (0, 0)][DBLP ] ESOP, 2006, pp:115-130 [Conf ] Cormac Flanagan , K. Rustan M. Leino Houdini, an Annotation Assistant for ESC/Java. [Citation Graph (0, 0)][DBLP ] FME, 2001, pp:500-517 [Conf ] K. Rustan M. Leino , Peter Müller Modular Verification of Static Class Invariants. [Citation Graph (0, 0)][DBLP ] FM, 2005, pp:26-42 [Conf ] Michael Barnett , Bor-Yuh Evan Chang , Robert DeLine , Bart Jacobs 0002 , K. Rustan M. Leino Boogie: A Modular Reusable Verifier for Object-Oriented Programs. [Citation Graph (0, 0)][DBLP ] FMCO, 2005, pp:364-387 [Conf ] K. Rustan M. Leino Challenges in Increasing Tool Support for Programming. [Citation Graph (0, 0)][DBLP ] ICTAC, 2004, pp:35-35 [Conf ] K. Rustan M. Leino , Rajeev Joshi A Semantic Approach to Secure Information Flow. [Citation Graph (0, 0)][DBLP ] MPC, 1998, pp:254-271 [Conf ] Manuel Fähndrich , K. Rustan M. Leino Declaring and checking non-null types in an object-oriented language. [Citation Graph (0, 0)][DBLP ] OOPSLA, 2003, pp:302-312 [Conf ] K. Rustan M. Leino Data Groups: Specifying the Modification of Extended State. [Citation Graph (0, 0)][DBLP ] OOPSLA, 1998, pp:144-153 [Conf ] Michael Barnett , K. Rustan M. Leino Weakest-precondition of unstructured programs. [Citation Graph (0, 0)][DBLP ] PASTE, 2005, pp:82-87 [Conf ] Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata Extended Static Checking for Java. [Citation Graph (0, 0)][DBLP ] PLDI, 2002, pp:234-245 [Conf ] K. Rustan M. Leino , Arnd Poetzsch-Heffter , Yunhong Zhou Using Data Groups to Specify and Check Side Effects. [Citation Graph (0, 0)][DBLP ] PLDI, 2002, pp:246-257 [Conf ] K. Rustan M. Leino Extended static checking. [Citation Graph (0, 0)][DBLP ] PROCOMET, 1998, pp:1-2 [Conf ] K. Rustan M. Leino , Jan L. A. van de Snepscheut Semantics of Exceptions. [Citation Graph (0, 0)][DBLP ] PROCOMET, 1994, pp:447-466 [Conf ] K. Rustan M. Leino Applications of Extended Static Checking. [Citation Graph (0, 0)][DBLP ] SAS, 2001, pp:185-193 [Conf ] K. Rustan M. Leino , Wolfram Schulte Exception Safety for C#. [Citation Graph (0, 0)][DBLP ] SEFM, 2004, pp:218-227 [Conf ] K. Rustan M. Leino Invariants on Demand. [Citation Graph (0, 0)][DBLP ] SEFM, 2005, pp:148-149 [Conf ] Bart Jacobs 0002 , Frank Piessens , K. Rustan M. Leino , Wolfram Schulte Safe Concurrency for Aggregate Objects with Invariants. [Citation Graph (0, 0)][DBLP ] SEFM, 2005, pp:137-147 [Conf ] K. Rustan M. Leino A SAT Characterization of Boolean-Program Correctness. [Citation Graph (0, 0)][DBLP ] SPIN, 2003, pp:104-120 [Conf ] K. Rustan M. Leino , Madan Musuvathi , Xinming Ou A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover. [Citation Graph (0, 0)][DBLP ] TACAS, 2005, pp:334-348 [Conf ] Martín Abadi , K. Rustan M. Leino A Logic of Object-Oriented Programs. [Citation Graph (0, 0)][DBLP ] TAPSOFT, 1997, pp:682-696 [Conf ] Bor-Yuh Evan Chang , K. Rustan M. Leino Abstract Interpretation with Alien Expressions and Heap Structures. [Citation Graph (0, 0)][DBLP ] VMCAI, 2005, pp:147-163 [Conf ] Michael Burrows , K. Rustan M. Leino Finding stale-value errors in concurrent programs. [Citation Graph (0, 0)][DBLP ] Concurrency - Practice and Experience, 2004, v:16, n:12, pp:1161-1172 [Journal ] Viktor Kuncak , K. Rustan M. Leino On computing the fixpoint of a set of boolean equations [Citation Graph (0, 0)][DBLP ] CoRR, 2004, v:0, n:, pp:- [Journal ] 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. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 2003, v:80, n:, pp:- [Journal ] Bor-Yuh Evan Chang , K. Rustan M. Leino Inferring Object Invariants: Extended Abstract. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 2005, v:131, n:, pp:63-74 [Journal ] K. Rustan M. Leino A Method for Showing Progress. [Citation Graph (0, 0)][DBLP ] Formal Asp. Comput., 1995, v:7, n:5, pp:576-580 [Journal ] K. Rustan M. Leino Computing Permutation Encodings. [Citation Graph (0, 0)][DBLP ] Formal Asp. Comput., 1999, v:11, n:1, pp:56-74 [Journal ] Rajit Manohar , K. Rustan M. Leino Conditional Composition. [Citation Graph (0, 0)][DBLP ] Formal Asp. Comput., 1995, v:7, n:6, pp:683-703 [Journal ] Cormac Flanagan , Rajeev Joshi , K. Rustan M. Leino Annotation inference for modular checkers. [Citation Graph (0, 0)][DBLP ] Inf. Process. Lett., 2001, v:77, n:2-4, pp:97-108 [Journal ] K. Rustan M. Leino Real estate of names. [Citation Graph (0, 0)][DBLP ] Inf. Process. Lett., 2001, v:77, n:2-4, pp:169-171 [Journal ] K. Rustan M. Leino Efficient weakest preconditions. [Citation Graph (0, 0)][DBLP ] Inf. Process. Lett., 2005, v:93, n:6, pp:281-288 [Journal ] K. Rustan M. Leino Constructing a Program with Exceptions. [Citation Graph (0, 0)][DBLP ] Inf. Process. Lett., 1995, v:53, n:3, pp:159-163 [Journal ] K. Rustan M. Leino , Raymie Stata Virginity: A Contribution to the Specification of Object-Oriented Software. [Citation Graph (0, 0)][DBLP ] Inf. Process. Lett., 1999, v:70, n:2, pp:99-105 [Journal ] Michael Barnett , Robert DeLine , Manuel Fähndrich , K. Rustan M. Leino , Wolfram Schulte Verification of Object-Oriented Programs with Invariants. [Citation Graph (0, 0)][DBLP ] Journal of Object Technology, 2004, v:3, n:6, pp:27-56 [Journal ] K. Rustan M. Leino Recursive Object Types in a Logic of Object-Oriented Programs. [Citation Graph (0, 0)][DBLP ] Nord. J. Comput., 1998, v:5, n:4, pp:330-360 [Journal ] Rajeev Joshi , K. Rustan M. Leino A semantic approach to secure information flow. [Citation Graph (0, 0)][DBLP ] Sci. Comput. Program., 2000, v:37, n:1-3, pp:113-138 [Journal ] K. Rustan M. Leino , Todd D. Millstein , James B. Saxe Generating error traces from verification-condition counterexamples. [Citation Graph (0, 0)][DBLP ] Sci. Comput. Program., 2005, v:55, n:1-3, pp:209-226 [Journal ] 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. [Citation Graph (0, 0)][DBLP ] STTT, 2005, v:7, n:3, pp:212-232 [Journal ] K. Rustan M. Leino , Rajit Manohar Joining Specification Statements. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 1999, v:216, n:1-2, pp:375-394 [Journal ] K. Rustan M. Leino , Greg Nelson Data abstraction and information hiding. [Citation Graph (0, 0)][DBLP ] ACM Trans. Program. Lang. Syst., 2002, v:24, n:5, pp:491-553 [Journal ] K. Rustan M. Leino Program Verification and Programming Methodology. [Citation Graph (0, 0)][DBLP ] Abstract State Machines, 2005, pp:73- [Conf ] K. Rustan M. Leino Designing Verification Conditions for Software. [Citation Graph (0, 0)][DBLP ] CADE, 2007, pp:345- [Conf ] K. Rustan M. Leino Specifying and Verifying Programs in Spec#. [Citation Graph (0, 0)][DBLP ] Ershov Memorial Conference, 2006, pp:20- [Conf ] K. Rustan M. Leino , Wolfram Schulte Using History Invariants to Verify Observers. [Citation Graph (0, 0)][DBLP ] ESOP, 2007, pp:80-94 [Conf ] Ádám Darvas , K. Rustan M. Leino Practical Reasoning About Invocations and Implementations of Pure Methods. [Citation Graph (0, 0)][DBLP ] FASE, 2007, pp:336-351 [Conf ] K. Rustan M. Leino Verifying Object-Oriented Software: Lessons and Challenges. [Citation Graph (0, 0)][DBLP ] TACAS, 2007, pp:2- [Conf ] Gary T. Leavens , K. Rustan M. Leino , Peter Müller Specification and verification challenges for sequential object-oriented programs. [Citation Graph (0, 0)][DBLP ] Formal Asp. Comput., 2007, v:19, n:2, pp:159-189 [Journal ] Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software Engineering. [Citation Graph (, )][DBLP ] Verification of Equivalent-Results Methods. [Citation Graph (, )][DBLP ] A Basis for Verifying Multi-threaded Programs. [Citation Graph (, )][DBLP ] Deadlock-Free Channels and Locks. [Citation Graph (, )][DBLP ] Proving Consistency of Pure Methods and Model Fields. [Citation Graph (, )][DBLP ] It's Doomed; We Can Prove It. [Citation Graph (, )][DBLP ] Verification of Concurrent Programs with Chalice. [Citation Graph (, )][DBLP ] Specifying and verifying software. [Citation Graph (, )][DBLP ] Reasoning about comprehensions with first-order SMT solvers. [Citation Graph (, )][DBLP ] A Polymorphic Intermediate Verification Language: Design and Logical Encoding. [Citation Graph (, )][DBLP ] HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier. [Citation Graph (, )][DBLP ] Verifying Concurrent Programs with Chalice. [Citation Graph (, )][DBLP ] Flexible Immutability with Frozen Objects. [Citation Graph (, )][DBLP ] To Goto Where No Statement Has Gone Before. [Citation Graph (, )][DBLP ] The Spec# Programming System: Challenges and Directions. [Citation Graph (, )][DBLP ] Dafny Meets the Verification Benchmarks Challenge. [Citation Graph (, )][DBLP ] Class-local object invariants. [Citation Graph (, )][DBLP ] Learning to do program verification. [Citation Graph (, )][DBLP ] Search in 0.009secs, Finished in 0.012secs