Reasoning about Comprehensions with First-Order SMT Solvers
Rustan Leino, Rosemary Monahan
SAC'09 March 8-12, 2009, Honolulu, Hawaii, U.S.A. | March 2009
Publications
Publications
Publications by Year
-
-
Verification of Equivalent-Results Methods
Rustan Leino, Peter Müller
March 2008
ISBN: 3-540-78738-0 978-3-540-78738-9
Class-Local Object Invariants
Rustan Leino, Angela Wallenburg
ISEC'08, February 19-22, 2008, Hyderabad, India. | February 2008
A Programming Model for Concurrent Object-Oriented Programs
Bart Jacobs, Frank Piessens, Jan Smans, Rustan Leino, Wolfram Schulte
ACM Trans. Program. Lang. Syst. | January 2008, Vol 31
-
Practical Reasoning About Invocations and Implementations of Pure Methods
Ádám Darvas, Rustan Leino
Proceeding: FASE'07 Proceedings of the 10th international conference on Fundamental approaches to software engineering | March 2007
ISBN: 978-3-540-71288-6
Automatic Verification of Textbook Programs that Use Comprehensions
Rustan Leino, Rosemary Monahan
In FTfJP '07: Proceedings of the 9th Workshop on Formal Techniques for Java-like Programs | January 2007
Using History Invariants to Verify Observers
Rustan Leino, Wolfram Schulte
ESOP | January 2007
ISBN: 978-3-540-71314-2
-
Building a Program Verifier
Rustan Leino, Shaz Qadeer
Guest lecture, Shaz Qadeer's cse599f, Formal Verification of Computer Systems, University of Washington, Seattle, WA | May 2006
A Verification Methodology for Model Fields
Rustan Leino, Peter Müller
Proceeding: ESOP'06 Proceedings of the 15th European conference on Programming Languages and Systems | March 2006
A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs
Wolfram Schulte
ICFEM | January 2006
ISBN: 3-540-47460-9
Discovering Likely Method Specifications
Nikolai Tillmann, Feng Chen, Wolfram Schulte
Proceedings of the 8th International Conference on Formal Engineering Methods (ICFEM'06), LNCS | January 2006
ISBN: 3-540-47460-9
-
The Spec# Programming System: Challenges and Directions
Mike Barnett, Robert DeLIne, Manuel Fähndrich, Bart Jacobs, Rustan Leino, Wolfram Schulte, Herman Venter
VSTTE 2005: Verified Software: Theories, Tools, Experiments | September 2005
Modular Verification of Static Class Invariants
Rustan Leino, Peter Müller
Proceeding: FM'05 Proceedings of the 2005 international conference on Formal Methods | July 2005
Inferring Object Invariants
Bor-Yuh Evan Chang, Rustan Leino
Electronic Notes in Theoretical Computer Science (ENTCS) | May 2005, Vol 131: pp. 63-74
Safe Concurrency for Aggregate Objects with Invariants
Bart Jacobs, Rustan Leino, Frank Piessens, Wolfram Schulte
SEFM | January 2005
ISBN: 0-7695-2435-4
The Spec# Programming System: An Overview
Mike Barnett, Rustan Leino, Wolfram Schulte
CASSIS 2004, Construction and Analysis of Safe, Secure and Interoperable Smart devices | January 2005
CASSIS 2004, Construction and Analysis of Safe, Secure and Interoperable Smart devices
-
Object Invariants in Dynamic Contexts
Rustan Leino, Peter Müller
ECOOP 2004 - Object-Oriented Programming | June 2004
Verification of Object-Oriented Programs With Invariants
Mike Barnett, Robert DeLIne, Manuel Fahndrich, Rustan Leino, Wolfram Schulte
Journal of Object Technology, Special issue | June 2004, Vol 3(6): pp. 27-56
Published as Technical Report 408 from ETH Zurich.
Exception Safety for C#
Rustan Leino, Wolfram Schulte
SEFM | January 2004
ISBN: 0-7695-2222-X
Publications by Research Area
-
Reasoning about Comprehensions with First-Order SMT Solvers
Rustan Leino, Rosemary Monahan
SAC'09 March 8-12, 2009, Honolulu, Hawaii, U.S.A. | March 2009
Verification of Equivalent-Results Methods
Rustan Leino, Peter Müller
March 2008
ISBN: 3-540-78738-0 978-3-540-78738-9
Class-Local Object Invariants
Rustan Leino, Angela Wallenburg
ISEC'08, February 19-22, 2008, Hyderabad, India. | February 2008
A Programming Model for Concurrent Object-Oriented Programs
Bart Jacobs, Frank Piessens, Jan Smans, Rustan Leino, Wolfram Schulte
ACM Trans. Program. Lang. Syst. | January 2008, Vol 31
Practical Reasoning About Invocations and Implementations of Pure Methods
Ádám Darvas, Rustan Leino
Proceeding: FASE'07 Proceedings of the 10th international conference on Fundamental approaches to software engineering | March 2007
ISBN: 978-3-540-71288-6
Automatic Verification of Textbook Programs that Use Comprehensions
Rustan Leino, Rosemary Monahan
In FTfJP '07: Proceedings of the 9th Workshop on Formal Techniques for Java-like Programs | January 2007
Using History Invariants to Verify Observers
Rustan Leino, Wolfram Schulte
ESOP | January 2007
ISBN: 978-3-540-71314-2
Building a Program Verifier
Rustan Leino, Shaz Qadeer
Guest lecture, Shaz Qadeer's cse599f, Formal Verification of Computer Systems, University of Washington, Seattle, WA | May 2006
A Verification Methodology for Model Fields
Rustan Leino, Peter Müller
Proceeding: ESOP'06 Proceedings of the 15th European conference on Programming Languages and Systems | March 2006
A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs
Wolfram Schulte
ICFEM | January 2006
ISBN: 3-540-47460-9
Discovering Likely Method Specifications
Nikolai Tillmann, Feng Chen, Wolfram Schulte
Proceedings of the 8th International Conference on Formal Engineering Methods (ICFEM'06), LNCS | January 2006
ISBN: 3-540-47460-9
The Spec# Programming System: Challenges and Directions
Mike Barnett, Robert DeLIne, Manuel Fähndrich, Bart Jacobs, Rustan Leino, Wolfram Schulte, Herman Venter
VSTTE 2005: Verified Software: Theories, Tools, Experiments | September 2005
Modular Verification of Static Class Invariants
Rustan Leino, Peter Müller
Proceeding: FM'05 Proceedings of the 2005 international conference on Formal Methods | July 2005
Inferring Object Invariants
Bor-Yuh Evan Chang, Rustan Leino
Electronic Notes in Theoretical Computer Science (ENTCS) | May 2005, Vol 131: pp. 63-74
Safe Concurrency for Aggregate Objects with Invariants
Bart Jacobs, Rustan Leino, Frank Piessens, Wolfram Schulte
SEFM | January 2005
ISBN: 0-7695-2435-4
The Spec# Programming System: An Overview
Mike Barnett, Rustan Leino, Wolfram Schulte
CASSIS 2004, Construction and Analysis of Safe, Secure and Interoperable Smart devices | January 2005
CASSIS 2004, Construction and Analysis of Safe, Secure and Interoperable Smart devices
Object Invariants in Dynamic Contexts
Rustan Leino, Peter Müller
ECOOP 2004 - Object-Oriented Programming | June 2004
Verification of Object-Oriented Programs With Invariants
Mike Barnett, Robert DeLIne, Manuel Fahndrich, Rustan Leino, Wolfram Schulte
Journal of Object Technology, Special issue | June 2004, Vol 3(6): pp. 27-56
Published as Technical Report 408 from ETH Zurich.
Exception Safety for C#
Rustan Leino, Wolfram Schulte
SEFM | January 2004
ISBN: 0-7695-2222-X
Publications by Type
-
Reasoning about Comprehensions with First-Order SMT Solvers
Rustan Leino, Rosemary Monahan
SAC'09 March 8-12, 2009, Honolulu, Hawaii, U.S.A. | March 2009
Verification of Equivalent-Results Methods
Rustan Leino, Peter Müller
March 2008
ISBN: 3-540-78738-0 978-3-540-78738-9
Class-Local Object Invariants
Rustan Leino, Angela Wallenburg
ISEC'08, February 19-22, 2008, Hyderabad, India. | February 2008
Practical Reasoning About Invocations and Implementations of Pure Methods
Ádám Darvas, Rustan Leino
Proceeding: FASE'07 Proceedings of the 10th international conference on Fundamental approaches to software engineering | March 2007
ISBN: 978-3-540-71288-6
Automatic Verification of Textbook Programs that Use Comprehensions
Rustan Leino, Rosemary Monahan
In FTfJP '07: Proceedings of the 9th Workshop on Formal Techniques for Java-like Programs | January 2007
Using History Invariants to Verify Observers
Rustan Leino, Wolfram Schulte
ESOP | January 2007
ISBN: 978-3-540-71314-2
Building a Program Verifier
Rustan Leino, Shaz Qadeer
Guest lecture, Shaz Qadeer's cse599f, Formal Verification of Computer Systems, University of Washington, Seattle, WA | May 2006
A Verification Methodology for Model Fields
Rustan Leino, Peter Müller
Proceeding: ESOP'06 Proceedings of the 15th European conference on Programming Languages and Systems | March 2006
A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs
Wolfram Schulte
ICFEM | January 2006
ISBN: 3-540-47460-9
Discovering Likely Method Specifications
Nikolai Tillmann, Feng Chen, Wolfram Schulte
Proceedings of the 8th International Conference on Formal Engineering Methods (ICFEM'06), LNCS | January 2006
ISBN: 3-540-47460-9
The Spec# Programming System: Challenges and Directions
Mike Barnett, Robert DeLIne, Manuel Fähndrich, Bart Jacobs, Rustan Leino, Wolfram Schulte, Herman Venter
VSTTE 2005: Verified Software: Theories, Tools, Experiments | September 2005
Modular Verification of Static Class Invariants
Rustan Leino, Peter Müller
Proceeding: FM'05 Proceedings of the 2005 international conference on Formal Methods | July 2005
Safe Concurrency for Aggregate Objects with Invariants
Bart Jacobs, Rustan Leino, Frank Piessens, Wolfram Schulte
SEFM | January 2005
ISBN: 0-7695-2435-4
The Spec# Programming System: An Overview
Mike Barnett, Rustan Leino, Wolfram Schulte
CASSIS 2004, Construction and Analysis of Safe, Secure and Interoperable Smart devices | January 2005
CASSIS 2004, Construction and Analysis of Safe, Secure and Interoperable Smart devices
Object Invariants in Dynamic Contexts
Rustan Leino, Peter Müller
ECOOP 2004 - Object-Oriented Programming | June 2004
Exception Safety for C#
Rustan Leino, Wolfram Schulte
SEFM | January 2004
ISBN: 0-7695-2222-X
-
A Programming Model for Concurrent Object-Oriented Programs
Bart Jacobs, Frank Piessens, Jan Smans, Rustan Leino, Wolfram Schulte
ACM Trans. Program. Lang. Syst. | January 2008, Vol 31
Inferring Object Invariants
Bor-Yuh Evan Chang, Rustan Leino
Electronic Notes in Theoretical Computer Science (ENTCS) | May 2005, Vol 131: pp. 63-74
Verification of Object-Oriented Programs With Invariants
Mike Barnett, Robert DeLIne, Manuel Fahndrich, Rustan Leino, Wolfram Schulte
Journal of Object Technology, Special issue | June 2004, Vol 3(6): pp. 27-56
Published as Technical Report 408 from ETH Zurich.
People
Rob DeLine
Senior Principal Researcher