Code Contracts

Verification Modulo Versions: Towards Usable Verification

Francesco Logozzo, Shuvendu Lahiri

Proceedings of the 35th conference on Programming Languages, Design, and Implementation (PLDI 2014) | June 2014

Publication Publication Project

Technology for Inferring Contracts from Code

Francesco Logozzo

Proceedings of SigADA High Integrity Language Technology (HILT 2013) | November 2013

Publication

Automatic Inference of Necessary Preconditions

Patrick Cousot, Radhia Cousot, Manuel Fahndrich, Francesco Logozzo

in Proceedings of the 14th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'13) | January 2013

Publication Publication

Inference of Necessary Field Conditions with Abstract Interpretation

Mehdi Bouaziz, Francesco Logozzo, Manuel Fahndrich

10th Asian Symposium on Programming Languages and Systems (APLAS 2012) | December 2012

10th Asian Symposium on Programming Languages and Systems (APLAS 2012)

Publication

An Abstract Interpretation Framework for Refactoring with Application to Extract Methods with Contracts

Patrick Cousot, Radhia Cousot, Francesco Logozzo, Mike Barnett

Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12) | October 2012

Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12)

Publication Publication

Modular and Verified Automatic Program Repair

Francesco Logozzo, Thomas Ball

Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12) | October 2012

Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12)

Publication Publication Video

A Semantic Integrated Development Environment

Francesco Logozzo, Manuel Fahndrich, Mike Barnett, Patric Cousot, Radhia Cousot

Companion of the Proceedings of the to the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012) | October 2012

Publication

Integrating a Set of Contract Checking Tools into Visual Studio

Manuel Fahndrich, Mike Barnett, Daan Leijen, Francesco Logozzo

Proceedings, Proceedings of the 2012 Second International Workshop on Developing Tools as Plug-ins (TOPI 2012) | June 2012

Publication

Checking Compatibility of Bit Sizes in Floating Point Comparison Operations

Manuel Fahndrich, Francesco Logozzo

Proceedings of the 3rd workshop on Numerical and Symbolic Abstract Domains | September 2011

Publication

SubPolyhedra: a family of numerical abstract domains for the (more) scalable inference of linear inequalities

Vincent Laviron, Francesco Logozzo

International Journal on Software Tools for Technology Transfer (STTT) | June 2011

Publication

A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis

Patrick Cousot, Radhia Cousot, Francesco Logozzo

Proceedings of the 38th Symposium on Programming Languages (POPL'11) | January 2011

Proceedings of the 38th Symposium on Programming Languages (POPL'11)

Publication Publication

Contract Precondition Inference from Intermittent Assertions on Collections

Patrick Cousot, Radhia Cousot, Francesco Logozzo

Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11) | January 2011

Publication

Practical verification for the working programmer with CodeContracts and Abstract Interpretation – Invited Talk

Francesco Logozzo

Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11) | January 2011

Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11)

Publication Publication

Static Contract Checking with Abstract Interpretation

Manuel Fahndrich, Francesco Logozzo

Proceedings of the Conference on Formal Verification of Object-oriented Software (FoVeOOS 2010) | October 2010

Publication Video

Static Verification for Code Contracts

Manuel Fahndrich

SAS'10 Proceedings of the 17th international conference on Static analysis | September 2010

Publication

Clousot: Static contract checking with Abstract Interpretation

Manuel Fahndrich, Francesco Logozzo

MSR-TR-2010-102 | June 2010

Formal Verification of Object-oriented software

Publication

Embedded Contract Languages

Manuel Fahndrich, Mike Barnett, Francesco Logozzo

ACM SAC - OOPS | March 2010

ACM SAC - OOPS

Publication

Refining Abstract Interpretation-based Static Analyses with Hints

Francesco Logozzo, Vincent Laviron

Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009) | December 2009

Publication

Exploiting the Synergy between Automated-Test-Generation and Programming-by-Contract

Mike Barnett, Manuel Fahndrich, Peli de Halleux, Francesco Logozzo, Nikolai Tillmann

Proc. 31st International Conference on Software Engineering (ICSE'2009) | May 2009

Proc. 31st International Conference on Software Engineering (ICSE'2009)

Research Demonstration

Publication Project Project

Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses

Francesco Logozzo, Manuel Fahndrich

Science of Computer Programming | January 2009

Publication

SubPolyhedra: A (more) scalable approach to infer linear inequalities

Vincent Laviron, Francesco Logozzo

Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'09) | January 2009

Publication Publication Download

Safer unsafe code for .NET

Pietro Ferrara, Francesco Logozzo, Manuel Fahndrich

Proceedings of the 23rd ACM Conference on Object-Oriented Programming (OOPSLA'08) | October 2008

Publication

Pentagons: A weakly relational domain for the efficient validation of array accesses

Francesco Logozzo, Manuel Fahndrich

Proceedings of the 23th ACM Symposium on Applied Computing | March 2008

Publication

On the Relative Completeness of Bytecode Analysis versus Source Code Analysis

Francesco Logozzo, Manuel Fahndrich

Proceedings of the International Conference on Compiler Construction | January 2008

Publication Publication

Verification Modulo Versions: Towards Usable Verification

Francesco Logozzo, Shuvendu Lahiri

Proceedings of the 35th conference on Programming Languages, Design, and Implementation (PLDI 2014) | June 2014

Publication Publication Project

Technology for Inferring Contracts from Code

Francesco Logozzo

Proceedings of SigADA High Integrity Language Technology (HILT 2013) | November 2013

Publication

Automatic Inference of Necessary Preconditions

Patrick Cousot, Radhia Cousot, Manuel Fahndrich, Francesco Logozzo

in Proceedings of the 14th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'13) | January 2013

Publication Publication

Inference of Necessary Field Conditions with Abstract Interpretation

Mehdi Bouaziz, Francesco Logozzo, Manuel Fahndrich

10th Asian Symposium on Programming Languages and Systems (APLAS 2012) | December 2012

10th Asian Symposium on Programming Languages and Systems (APLAS 2012)

Publication

An Abstract Interpretation Framework for Refactoring with Application to Extract Methods with Contracts

Patrick Cousot, Radhia Cousot, Francesco Logozzo, Mike Barnett

Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12) | October 2012

Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12)

Publication Publication

Modular and Verified Automatic Program Repair

Francesco Logozzo, Thomas Ball

Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12) | October 2012

Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12)

Publication Publication Video

A Semantic Integrated Development Environment

Francesco Logozzo, Manuel Fahndrich, Mike Barnett, Patric Cousot, Radhia Cousot

Companion of the Proceedings of the to the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012) | October 2012

Publication

Integrating a Set of Contract Checking Tools into Visual Studio

Manuel Fahndrich, Mike Barnett, Daan Leijen, Francesco Logozzo

Proceedings, Proceedings of the 2012 Second International Workshop on Developing Tools as Plug-ins (TOPI 2012) | June 2012

Publication

Checking Compatibility of Bit Sizes in Floating Point Comparison Operations

Manuel Fahndrich, Francesco Logozzo

Proceedings of the 3rd workshop on Numerical and Symbolic Abstract Domains | September 2011

Publication

SubPolyhedra: a family of numerical abstract domains for the (more) scalable inference of linear inequalities

Vincent Laviron, Francesco Logozzo

International Journal on Software Tools for Technology Transfer (STTT) | June 2011

Publication

A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis

Patrick Cousot, Radhia Cousot, Francesco Logozzo

Proceedings of the 38th Symposium on Programming Languages (POPL'11) | January 2011

Proceedings of the 38th Symposium on Programming Languages (POPL'11)

Publication Publication

Contract Precondition Inference from Intermittent Assertions on Collections

Patrick Cousot, Radhia Cousot, Francesco Logozzo

Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11) | January 2011

Publication

Practical verification for the working programmer with CodeContracts and Abstract Interpretation – Invited Talk

Francesco Logozzo

Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11) | January 2011

Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11)

Publication Publication

Static Contract Checking with Abstract Interpretation

Manuel Fahndrich, Francesco Logozzo

Proceedings of the Conference on Formal Verification of Object-oriented Software (FoVeOOS 2010) | October 2010

Publication Video

Static Verification for Code Contracts

Manuel Fahndrich

SAS'10 Proceedings of the 17th international conference on Static analysis | September 2010

Publication

Clousot: Static contract checking with Abstract Interpretation

Manuel Fahndrich, Francesco Logozzo

MSR-TR-2010-102 | June 2010

Formal Verification of Object-oriented software

Publication

Embedded Contract Languages

Manuel Fahndrich, Mike Barnett, Francesco Logozzo

ACM SAC - OOPS | March 2010

ACM SAC - OOPS

Publication

Refining Abstract Interpretation-based Static Analyses with Hints

Francesco Logozzo, Vincent Laviron

Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009) | December 2009

Publication

Exploiting the Synergy between Automated-Test-Generation and Programming-by-Contract

Mike Barnett, Manuel Fahndrich, Peli de Halleux, Francesco Logozzo, Nikolai Tillmann

Proc. 31st International Conference on Software Engineering (ICSE'2009) | May 2009

Proc. 31st International Conference on Software Engineering (ICSE'2009)

Research Demonstration

Publication Project Project

Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses

Francesco Logozzo, Manuel Fahndrich

Science of Computer Programming | January 2009

Publication

SubPolyhedra: A (more) scalable approach to infer linear inequalities

Vincent Laviron, Francesco Logozzo

Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'09) | January 2009

Publication Publication Download

Safer unsafe code for .NET

Pietro Ferrara, Francesco Logozzo, Manuel Fahndrich

Proceedings of the 23rd ACM Conference on Object-Oriented Programming (OOPSLA'08) | October 2008

Publication

Pentagons: A weakly relational domain for the efficient validation of array accesses

Francesco Logozzo, Manuel Fahndrich

Proceedings of the 23th ACM Symposium on Applied Computing | March 2008

Publication

On the Relative Completeness of Bytecode Analysis versus Source Code Analysis

Francesco Logozzo, Manuel Fahndrich

Proceedings of the International Conference on Compiler Construction | January 2008

Publication Publication

Verification Modulo Versions: Towards Usable Verification

Francesco Logozzo, Shuvendu Lahiri

Proceedings of the 35th conference on Programming Languages, Design, and Implementation (PLDI 2014) | June 2014

Publication Publication Project

Technology for Inferring Contracts from Code

Francesco Logozzo

Proceedings of SigADA High Integrity Language Technology (HILT 2013) | November 2013

Publication

Automatic Inference of Necessary Preconditions

Patrick Cousot, Radhia Cousot, Manuel Fahndrich, Francesco Logozzo

in Proceedings of the 14th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'13) | January 2013

Publication Publication

Inference of Necessary Field Conditions with Abstract Interpretation

Mehdi Bouaziz, Francesco Logozzo, Manuel Fahndrich

10th Asian Symposium on Programming Languages and Systems (APLAS 2012) | December 2012

10th Asian Symposium on Programming Languages and Systems (APLAS 2012)

Publication

An Abstract Interpretation Framework for Refactoring with Application to Extract Methods with Contracts

Patrick Cousot, Radhia Cousot, Francesco Logozzo, Mike Barnett

Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12) | October 2012

Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12)

Publication Publication

Modular and Verified Automatic Program Repair

Francesco Logozzo, Thomas Ball

Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12) | October 2012

Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12)

Publication Publication Video

A Semantic Integrated Development Environment

Francesco Logozzo, Manuel Fahndrich, Mike Barnett, Patric Cousot, Radhia Cousot

Companion of the Proceedings of the to the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012) | October 2012

Publication

Integrating a Set of Contract Checking Tools into Visual Studio

Manuel Fahndrich, Mike Barnett, Daan Leijen, Francesco Logozzo

Proceedings, Proceedings of the 2012 Second International Workshop on Developing Tools as Plug-ins (TOPI 2012) | June 2012

Publication

Checking Compatibility of Bit Sizes in Floating Point Comparison Operations

Manuel Fahndrich, Francesco Logozzo

Proceedings of the 3rd workshop on Numerical and Symbolic Abstract Domains | September 2011

Publication

SubPolyhedra: a family of numerical abstract domains for the (more) scalable inference of linear inequalities

Vincent Laviron, Francesco Logozzo

International Journal on Software Tools for Technology Transfer (STTT) | June 2011

Publication

A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis

Patrick Cousot, Radhia Cousot, Francesco Logozzo

Proceedings of the 38th Symposium on Programming Languages (POPL'11) | January 2011

Proceedings of the 38th Symposium on Programming Languages (POPL'11)

Publication Publication

Contract Precondition Inference from Intermittent Assertions on Collections

Patrick Cousot, Radhia Cousot, Francesco Logozzo

Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11) | January 2011

Publication

Practical verification for the working programmer with CodeContracts and Abstract Interpretation – Invited Talk

Francesco Logozzo

Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11) | January 2011

Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11)

Publication Publication

Static Contract Checking with Abstract Interpretation

Manuel Fahndrich, Francesco Logozzo

Proceedings of the Conference on Formal Verification of Object-oriented Software (FoVeOOS 2010) | October 2010

Publication Video

Static Verification for Code Contracts

Manuel Fahndrich

SAS'10 Proceedings of the 17th international conference on Static analysis | September 2010

Publication

Embedded Contract Languages

Manuel Fahndrich, Mike Barnett, Francesco Logozzo

ACM SAC - OOPS | March 2010

ACM SAC - OOPS

Publication

Refining Abstract Interpretation-based Static Analyses with Hints

Francesco Logozzo, Vincent Laviron

Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009) | December 2009

Publication

Exploiting the Synergy between Automated-Test-Generation and Programming-by-Contract

Mike Barnett, Manuel Fahndrich, Peli de Halleux, Francesco Logozzo, Nikolai Tillmann

Proc. 31st International Conference on Software Engineering (ICSE'2009) | May 2009

Proc. 31st International Conference on Software Engineering (ICSE'2009)

Research Demonstration

Publication Project Project

SubPolyhedra: A (more) scalable approach to infer linear inequalities

Vincent Laviron, Francesco Logozzo

Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'09) | January 2009

Publication Publication Download

Safer unsafe code for .NET

Pietro Ferrara, Francesco Logozzo, Manuel Fahndrich

Proceedings of the 23rd ACM Conference on Object-Oriented Programming (OOPSLA'08) | October 2008

Publication

Pentagons: A weakly relational domain for the efficient validation of array accesses

Francesco Logozzo, Manuel Fahndrich

Proceedings of the 23th ACM Symposium on Applied Computing | March 2008

Publication

On the Relative Completeness of Bytecode Analysis versus Source Code Analysis

Francesco Logozzo, Manuel Fahndrich

Proceedings of the International Conference on Compiler Construction | January 2008

Publication Publication

Clousot: Static contract checking with Abstract Interpretation

Manuel Fahndrich, Francesco Logozzo

MSR-TR-2010-102 | June 2010

Formal Verification of Object-oriented software

Publication

Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses

Francesco Logozzo, Manuel Fahndrich

Science of Computer Programming | January 2009

Publication