Search    Browse

The FacetedDBLP logo    Search for: in:

Disable automatic phrases ?     Syntactic query expansion: ?

Publications of "K. Rustan M. Leino" ( http://dblp.L3S.de/Authors/K._Rustan_M._Leino )

URL (Homepage):  http://research.microsoft.com/~leino/  Author page on DBLP  Author page in RDF  Community of K. Rustan M. Leino in ASPL-2

Publication years (Num. hits)
1994-1999 (15) 2000-2004 (19) 2005-2006 (16) 2007-2009 (18) 2010-2012 (16)
Publication types (Num. hits)
article(24) inproceedings(59) proceedings(1)
Venues (Conferences, Journals, ...)
ESOP(6) Inf. Process. Lett.(5) VSTTE(5) Formal Asp. Comput.(4) SEFM(4) TACAS(4) FM(3) VMCAI(3) ACM Trans. Program. Lang. Syst...(2) Commun. ACM(2) Electr. Notes Theor. Comput. S...(2) FASE(2) OOPSLA(2) PLDI(2) PROCOMET(2) Sci. Comput. Program.(2) More (+10 of total 50)
Authors
K. Rustan M. Leino(84) Peter Müller(12) Wolfram Schulte(7) Michael Barnett(5) Bart Jacobs 0002(4) Gary T. Leavens(4) Jan Smans(4) Manuel Fähndrich(4) Bor-Yuh Evan Chang(3) Cormac Flanagan(3) Frank Piessens(3) Greg Nelson(3) James B. Saxe(3) Rajeev Joshi(3) Raymie Stata(3) Robert DeLine(3) More (+10 of total 67)
GrowBag graphs for keyword ? (Num. hits/coverage)

Group by:
The graphs summarize 40 occurrences of 28 keywords
Results
Found 84 publication records. Showing 84 according to the selection in the facets
Hits ?▲ Authors Title Venue Year Link Author keywords
1K. Rustan M. Leino Developing Verified Programs with Dafny. Search on Bibsonomy VSTTE The full citation details ... 2012 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Automating Induction with an SMT Solver. Search on Bibsonomy VMCAI The full citation details ... 2012 DBLP  DOI  BibTeX  RDF
1Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, Herman Venter Specification and verification: the Spec# experience. Search on Bibsonomy Commun. ACM The full citation details ... 2011 DBLP  DOI  BibTeX  RDF
1Claire Le Goues, K. Rustan M. Leino, Michal Moskal The Boogie Verification Debugger (Tool Paper). Search on Bibsonomy SEFM The full citation details ... 2011 DBLP  DOI  BibTeX  RDF
1Parosh Aziz Abdulla, K. Rustan M. Leino (eds.) 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 Search on Bibsonomy TACAS The full citation details ... 2011 DBLP  DOI  BibTeX  RDF
1Vladimir 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. Search on Bibsonomy FM The full citation details ... 2011 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino From Retrospective Verification to Forward-Looking Development. Search on Bibsonomy NASA Formal Methods The full citation details ... 2011 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Learning to do program verification. Search on Bibsonomy Commun. ACM The full citation details ... 2010 DBLP  DOI  BibTeX  RDF
1Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies Doomed program points. Search on Bibsonomy Formal Methods in System Design The full citation details ... 2010 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Philipp Rümmer A Polymorphic Intermediate Verification Language: Design and Logical Encoding. Search on Bibsonomy TACAS The full citation details ... 2010 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Dafny: An Automatic Program Verifier for Functional Correctness. Search on Bibsonomy LPAR (Dakar) The full citation details ... 2010 DBLP  DOI  BibTeX  RDF
1Michael Barnett, K. Rustan M. Leino To Goto Where No Statement Has Gone Before. Search on Bibsonomy VSTTE The full citation details ... 2010 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Rosemary Monahan Dafny Meets the Verification Benchmarks Challenge. Search on Bibsonomy VSTTE The full citation details ... 2010 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Tools and Behavioral Abstraction: A Direction for Software Engineering. Search on Bibsonomy The Future of Software Engineering The full citation details ... 2010 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Verifying Concurrent Programs with Chalice. Search on Bibsonomy VMCAI The full citation details ... 2010 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Peter Müller, Jan Smans Deadlock-Free Channels and Locks. Search on Bibsonomy ESOP The full citation details ... 2010 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Rosemary Monahan Reasoning about comprehensions with first-order SMT solvers. Search on Bibsonomy SAC The full citation details ... 2009 DBLP  DOI  BibTeX  RDF Spec#, matching triggers, quantifiers, SMT solvers
1K. Rustan M. Leino, Peter Müller, Jan Smans Verification of Concurrent Programs with Chalice. Search on Bibsonomy FOSAD The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Ronald Middelkoop Proving Consistency of Pure Methods and Model Fields. Search on Bibsonomy FASE The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies It's Doomed; We Can Prove It. Search on Bibsonomy FM The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Peter Müller A Basis for Verifying Multi-threaded Programs. Search on Bibsonomy ESOP The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Bart Jacobs 0002, Frank Piessens, Jan Smans, K. Rustan M. Leino, Wolfram Schulte A programming model for concurrent object-oriented programs. Search on Bibsonomy ACM Trans. Program. Lang. Syst. The full citation details ... 2008 DBLP  DOI  BibTeX  RDF verification condition generation, Aliasing, data races, ownership, modular reasoning, local reasoning
1K. Rustan M. Leino, Angela Wallenburg Class-local object invariants. Search on Bibsonomy ISEC The full citation details ... 2008 DBLP  DOI  BibTeX  RDF verification, object-oriented programming, specification, automation, tool support, subclassing
1K. Rustan M. Leino Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software Engineering. Search on Bibsonomy COMPSAC The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Peter Müller Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs. Search on Bibsonomy LASER Summer School The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Peter Müller, Angela Wallenburg Flexible Immutability with Frozen Objects. Search on Bibsonomy VSTTE The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Peter Müller Verification of Equivalent-Results Methods. Search on Bibsonomy ESOP The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Gary T. Leavens, K. Rustan M. Leino, Peter Müller Specification and verification challenges for sequential object-oriented programs. Search on Bibsonomy Formal Asp. Comput. The full citation details ... 2007 DBLP  DOI  BibTeX  RDF Object-oriented programming, Specification, Program verification, Contract, Challenge
1K. Rustan M. Leino Designing Verification Conditions for Software. Search on Bibsonomy CADE The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Verifying Object-Oriented Software: Lessons and Challenges. Search on Bibsonomy TACAS The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Specifying and verifying software. Search on Bibsonomy ASE The full citation details ... 2007 DBLP  DOI  BibTeX  RDF verification, specification, programming, automation, languages, tool support, SMT solver
1Ádám Darvas, K. Rustan M. Leino Practical Reasoning About Invocations and Implementations of Pure Methods. Search on Bibsonomy FASE The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Wolfram Schulte Using History Invariants to Verify Observers. Search on Bibsonomy ESOP The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Specifying and Verifying Programs in Spec#. Search on Bibsonomy Ershov Memorial Conference The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Peter Müller A Verification Methodology for Model Fields. Search on Bibsonomy ESOP The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Efficient weakest preconditions. Search on Bibsonomy Inf. Process. Lett. The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Todd D. Millstein, James B. Saxe Generating error traces from verification-condition counterexamples. Search on Bibsonomy Sci. Comput. Program. The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1Bor-Yuh Evan Chang, K. Rustan M. Leino Inferring Object Invariants: Extended Abstract. Search on Bibsonomy Electr. Notes Theor. Comput. Sci. The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1Lilian 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. Search on Bibsonomy STTT The full citation details ... 2005 DBLP  DOI  BibTeX  RDF Assertion checking, Java, Formal specification, Program verification, Design by Contract
1K. Rustan M. Leino Invariants on Demand. Search on Bibsonomy SEFM The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1Bart Jacobs 0002, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte Safe Concurrency for Aggregate Objects with Invariants. Search on Bibsonomy SEFM The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Madan Musuvathi, Xinming Ou A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover. Search on Bibsonomy TACAS The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs 0002, K. Rustan M. Leino Boogie: A Modular Reusable Verifier for Object-Oriented Programs. Search on Bibsonomy FMCO The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1Michael Barnett, Robert DeLine, Manuel Fähndrich, Bart Jacobs 0002, K. Rustan M. Leino, Wolfram Schulte, Herman Venter The Spec# Programming System: Challenges and Directions. Search on Bibsonomy VSTTE The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Peter Müller Modular Verification of Static Class Invariants. Search on Bibsonomy FM The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1Michael Barnett, K. Rustan M. Leino Weakest-precondition of unstructured programs. Search on Bibsonomy PASTE The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Francesco Logozzo Loop Invariants on Demand. Search on Bibsonomy APLAS The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1Bor-Yuh Evan Chang, K. Rustan M. Leino Abstract Interpretation with Alien Expressions and Heap Structures. Search on Bibsonomy VMCAI The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Program Verification and Programming Methodology. Search on Bibsonomy Abstract State Machines The full citation details ... 2005 DBLP  BibTeX  RDF
1Michael Burrows, K. Rustan M. Leino Finding stale-value errors in concurrent programs. Search on Bibsonomy Concurrency - Practice and Experience The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
1Michael Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte Verification of Object-Oriented Programs with Invariants. Search on Bibsonomy Journal of Object Technology The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
1Viktor Kuncak, K. Rustan M. Leino On computing the fixpoint of a set of boolean equations Search on Bibsonomy CoRR The full citation details ... 2004 DBLP  BibTeX  RDF
1K. Rustan M. Leino, Wolfram Schulte Exception Safety for C#. Search on Bibsonomy SEFM The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Challenges in Increasing Tool Support for Programming. Search on Bibsonomy ICTAC The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Peter Müller Object Invariants in Dynamic Contexts. Search on Bibsonomy ECOOP The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
1Lilian 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. Search on Bibsonomy Electr. Notes Theor. Comput. Sci. The full citation details ... 2003 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino A SAT Characterization of Boolean-Program Correctness. Search on Bibsonomy SPIN The full citation details ... 2003 DBLP  DOI  BibTeX  RDF
1Manuel Fähndrich, K. Rustan M. Leino Declaring and checking non-null types in an object-oriented language. Search on Bibsonomy OOPSLA The full citation details ... 2003 DBLP  DOI  BibTeX  RDF non-null types, null references, Java, type system, c#
1Martín Abadi, K. Rustan M. Leino A Logic of Object-Oriented Programs. Search on Bibsonomy Verification: Theory and Practice The full citation details ... 2003 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Greg Nelson Data abstraction and information hiding. Search on Bibsonomy ACM Trans. Program. Lang. Syst. The full citation details ... 2002 DBLP  DOI  BibTeX  RDF Abstract variables, abstraction dependencies, modifies clauses, object-oriented programming, specifications, modular verification, extended static checking
1K. Rustan M. Leino, Arnd Poetzsch-Heffter, Yunhong Zhou Using Data Groups to Specify and Check Side Effects. Search on Bibsonomy PLDI The full citation details ... 2002 DBLP  DOI  BibTeX  RDF alias confinement, data groups, frame conditions, modifies lists, modular soundness, owner exclusion, pivot uniqueness, verification, side effects
1Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata Extended Static Checking for Java. Search on Bibsonomy PLDI The full citation details ... 2002 DBLP  DOI  BibTeX  RDF compile-time program checking
1K. Rustan M. Leino Real estate of names. Search on Bibsonomy Inf. Process. Lett. The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
1Cormac Flanagan, Rajeev Joshi, K. Rustan M. Leino Annotation inference for modular checkers. Search on Bibsonomy Inf. Process. Lett. The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Extended Static Checking: A Ten-Year Perspective. Search on Bibsonomy Informatics The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
1Cormac Flanagan, K. Rustan M. Leino Houdini, an Annotation Assistant for ESC/Java. Search on Bibsonomy FME The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Applications of Extended Static Checking. Search on Bibsonomy SAS The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
1Rajeev Joshi, K. Rustan M. Leino A semantic approach to secure information flow. Search on Bibsonomy Sci. Comput. Program. The full citation details ... 2000 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Computing Permutation Encodings. Search on Bibsonomy Formal Asp. Comput. The full citation details ... 1999 DBLP  DOI  BibTeX  RDF Permutation encodings, Inversion table, Code of an array, Program derivation, Program inversion
1K. Rustan M. Leino, Raymie Stata Virginity: A Contribution to the Specification of Object-Oriented Software. Search on Bibsonomy Inf. Process. Lett. The full citation details ... 1999 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Rajit Manohar Joining Specification Statements. Search on Bibsonomy Theor. Comput. Sci. The full citation details ... 1999 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, James B. Saxe, Raymie Stata Checking Java Programs via Guarded Commands. Search on Bibsonomy ECOOP Workshops The full citation details ... 1999 DBLP  BibTeX  RDF
1K. Rustan M. Leino Recursive Object Types in a Logic of Object-Oriented Programs. Search on Bibsonomy Nord. J. Comput. The full citation details ... 1998 DBLP  BibTeX  RDF
1K. Rustan M. Leino Extended static checking. Search on Bibsonomy PROCOMET The full citation details ... 1998 DBLP  BibTeX  RDF
1K. Rustan M. Leino, Greg Nelson An Extended Static Checker for Modular-3. Search on Bibsonomy CC The full citation details ... 1998 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Data Groups: Specifying the Modification of Extended State. Search on Bibsonomy OOPSLA The full citation details ... 1998 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Rajeev Joshi A Semantic Approach to Secure Information Flow. Search on Bibsonomy MPC The full citation details ... 1998 DBLP  BibTeX  RDF
1K. Rustan M. Leino Recursive Object Types in a Logic of Object-Oriented Programs. Search on Bibsonomy ESOP The full citation details ... 1998 DBLP  DOI  BibTeX  RDF
1Martín Abadi, K. Rustan M. Leino A Logic of Object-Oriented Programs. Search on Bibsonomy TAPSOFT The full citation details ... 1997 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino A Method for Showing Progress. Search on Bibsonomy Formal Asp. Comput. The full citation details ... 1995 DBLP  DOI  BibTeX  RDF
1Rajit Manohar, K. Rustan M. Leino Conditional Composition. Search on Bibsonomy Formal Asp. Comput. The full citation details ... 1995 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino Constructing a Program with Exceptions. Search on Bibsonomy Inf. Process. Lett. The full citation details ... 1995 DBLP  DOI  BibTeX  RDF
1K. Rustan M. Leino, Jan L. A. van de Snepscheut Semantics of Exceptions. Search on Bibsonomy PROCOMET The full citation details ... 1994 DBLP  BibTeX  RDF
Displaying result #1 - #84 of 84 (100 per page; Change: )
Valid XHTML 1.1! Valid CSS! [Valid RSS]
Maintained by Jörg Diederich.
Based upon DBLP by Michael Ley.