Spec#

Established: June 11, 2004

Publications

View by:

- 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
  
  Publication Publication
- Verification of Equivalent-Results Methods
  
  Rustan Leino, Peter Müller
  
  March 2008
  
  ISBN: 3-540-78738-0 978-3-540-78738-9
  
  Publication
- Class-Local Object Invariants
  
  Rustan Leino, Angela Wallenburg
  
  ISEC'08, February 19-22, 2008, Hyderabad, India. | February 2008
  
  Publication Publication
- 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
  
  Publication Project
- 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
  
  Publication
- 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
  
  Publication Publication
- Using History Invariants to Verify Observers
  
  Rustan Leino, Wolfram Schulte
  
  ESOP | January 2007
  
  ISBN: 978-3-540-71314-2
  
  Publication Publication
- 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
  
  Publication Publication
- 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
  
  Publication Publication
- A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs
  
  Wolfram Schulte
  
  ICFEM | January 2006
  
  ISBN: 3-540-47460-9
  
  Publication
- 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
  
  Publication Publication Project Project
- 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
  
  Publication Publication Publication Publication
- 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
  
  Publication Publication
- Inferring Object Invariants
  
  Bor-Yuh Evan Chang, Rustan Leino
  
  Electronic Notes in Theoretical Computer Science (ENTCS) | May 2005, Vol 131: pp. 63-74
  
  Publication Publication
- Safe Concurrency for Aggregate Objects with Invariants
  
  Bart Jacobs, Rustan Leino, Frank Piessens, Wolfram Schulte
  
  SEFM | January 2005
  
  ISBN: 0-7695-2435-4
  
  Publication
- 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
  
  Publication
- Object Invariants in Dynamic Contexts
  
  Rustan Leino, Peter Müller
  
  ECOOP 2004 - Object-Oriented Programming | June 2004
  
  Publication
- 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.
  
  Publication Publication
- Exception Safety for C#
  
  Rustan Leino, Wolfram Schulte
  
  SEFM | January 2004
  
  ISBN: 0-7695-2222-X
  
  Publication

- 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
  
  Publication Publication
- Verification of Equivalent-Results Methods
  
  Rustan Leino, Peter Müller
  
  March 2008
  
  ISBN: 3-540-78738-0 978-3-540-78738-9
  
  Publication
- Class-Local Object Invariants
  
  Rustan Leino, Angela Wallenburg
  
  ISEC'08, February 19-22, 2008, Hyderabad, India. | February 2008
  
  Publication Publication
- 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
  
  Publication Project
- 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
  
  Publication
- 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
  
  Publication Publication
- Using History Invariants to Verify Observers
  
  Rustan Leino, Wolfram Schulte
  
  ESOP | January 2007
  
  ISBN: 978-3-540-71314-2
  
  Publication Publication
- 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
  
  Publication Publication
- 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
  
  Publication Publication
- 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
  
  Publication Publication Project Project
- A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs
  
  Wolfram Schulte
  
  ICFEM | January 2006
  
  ISBN: 3-540-47460-9
  
  Publication
- 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
  
  Publication Publication Publication Publication
- 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
  
  Publication Publication
- Inferring Object Invariants
  
  Bor-Yuh Evan Chang, Rustan Leino
  
  Electronic Notes in Theoretical Computer Science (ENTCS) | May 2005, Vol 131: pp. 63-74
  
  Publication Publication
- 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
  
  Publication
- Safe Concurrency for Aggregate Objects with Invariants
  
  Bart Jacobs, Rustan Leino, Frank Piessens, Wolfram Schulte
  
  SEFM | January 2005
  
  ISBN: 0-7695-2435-4
  
  Publication
- Object Invariants in Dynamic Contexts
  
  Rustan Leino, Peter Müller
  
  ECOOP 2004 - Object-Oriented Programming | June 2004
  
  Publication
- 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.
  
  Publication Publication
- Exception Safety for C#
  
  Rustan Leino, Wolfram Schulte
  
  SEFM | January 2004
  
  ISBN: 0-7695-2222-X
  
  Publication

- 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
  
  Publication Publication
- Verification of Equivalent-Results Methods
  
  Rustan Leino, Peter Müller
  
  March 2008
  
  ISBN: 3-540-78738-0 978-3-540-78738-9
  
  Publication
- Class-Local Object Invariants
  
  Rustan Leino, Angela Wallenburg
  
  ISEC'08, February 19-22, 2008, Hyderabad, India. | February 2008
  
  Publication Publication
- 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
  
  Publication
- 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
  
  Publication Publication
- Using History Invariants to Verify Observers
  
  Rustan Leino, Wolfram Schulte
  
  ESOP | January 2007
  
  ISBN: 978-3-540-71314-2
  
  Publication Publication
- 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
  
  Publication Publication
- 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
  
  Publication Publication
- 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
  
  Publication Publication Project Project
- A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs
  
  Wolfram Schulte
  
  ICFEM | January 2006
  
  ISBN: 3-540-47460-9
  
  Publication
- 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
  
  Publication Publication Publication Publication
- 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
  
  Publication Publication
- 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
  
  Publication
- Safe Concurrency for Aggregate Objects with Invariants
  
  Bart Jacobs, Rustan Leino, Frank Piessens, Wolfram Schulte
  
  SEFM | January 2005
  
  ISBN: 0-7695-2435-4
  
  Publication
- Object Invariants in Dynamic Contexts
  
  Rustan Leino, Peter Müller
  
  ECOOP 2004 - Object-Oriented Programming | June 2004
  
  Publication
- Exception Safety for C#
  
  Rustan Leino, Wolfram Schulte
  
  SEFM | January 2004
  
  ISBN: 0-7695-2222-X
  
  Publication
- 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
  
  Publication Project
- Inferring Object Invariants
  
  Bor-Yuh Evan Chang, Rustan Leino
  
  Electronic Notes in Theoretical Computer Science (ENTCS) | May 2005, Vol 131: pp. 63-74
  
  Publication Publication
- 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.
  
  Publication Publication

Spec#

Publications

Reasoning about Comprehensions with First-Order SMT Solvers

Verification of Equivalent-Results Methods

Class-Local Object Invariants

A Programming Model for Concurrent Object-Oriented Programs

Practical Reasoning About Invocations and Implementations of Pure Methods

Automatic Verification of Textbook Programs that Use Comprehensions

Using History Invariants to Verify Observers

Building a Program Verifier

A Verification Methodology for Model Fields

A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs

Discovering Likely Method Specifications

The Spec# Programming System: Challenges and Directions

Modular Verification of Static Class Invariants

Inferring Object Invariants

Safe Concurrency for Aggregate Objects with Invariants

The Spec# Programming System: An Overview

Object Invariants in Dynamic Contexts

Verification of Object-Oriented Programs With Invariants

Exception Safety for C#

Reasoning about Comprehensions with First-Order SMT Solvers

Verification of Equivalent-Results Methods

Class-Local Object Invariants

A Programming Model for Concurrent Object-Oriented Programs

Practical Reasoning About Invocations and Implementations of Pure Methods

Automatic Verification of Textbook Programs that Use Comprehensions

Using History Invariants to Verify Observers

Building a Program Verifier

A Verification Methodology for Model Fields

Discovering Likely Method Specifications

A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs

The Spec# Programming System: Challenges and Directions

Modular Verification of Static Class Invariants

Inferring Object Invariants

The Spec# Programming System: An Overview

Safe Concurrency for Aggregate Objects with Invariants

Object Invariants in Dynamic Contexts

Verification of Object-Oriented Programs With Invariants

Exception Safety for C#

Reasoning about Comprehensions with First-Order SMT Solvers

Verification of Equivalent-Results Methods

Class-Local Object Invariants

Practical Reasoning About Invocations and Implementations of Pure Methods

Automatic Verification of Textbook Programs that Use Comprehensions

Using History Invariants to Verify Observers

Building a Program Verifier

A Verification Methodology for Model Fields

Discovering Likely Method Specifications

A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs

The Spec# Programming System: Challenges and Directions

Modular Verification of Static Class Invariants

The Spec# Programming System: An Overview

Safe Concurrency for Aggregate Objects with Invariants

Object Invariants in Dynamic Contexts

Exception Safety for C#

A Programming Model for Concurrent Object-Oriented Programs

Inferring Object Invariants

Verification of Object-Oriented Programs With Invariants