FuncTion

Programming errors which cause non-termination can compromise software systems by making them irresponsive. Notorious examples are the Microsoft Zune Z2K bug[1] and the Microsoft Azure Storage service interruption[2]. Termination bugs can also be exploited in denial-of-service attacks[3]. Therefore, proving program termination is important for ensuring software reliability.

FuncTion

The traditional method for proving termination is based on the synthesis of a ranking function, a well-founded metric which strictly decreases during the program execution. The goal of the project was the development of a static analyzer which automatically infers ranking functions and sufficient precondition for program termination (and other liveness properties) by means of abstract interpretation. The static analyzer is open-source and available on GitHub.

Completed Projects

Publications

. Automatic Detection of Vulnerable Variables for CTL Properties of Programs. In LPAR, 2024.

PDF Code Project Artifact HAL EasyChair

. Abstract Interpretation of CTL Properties. In SAS, 2018.

PDF Code Project Video Artifact BibTeX Springer FuncTion

. Precise Widening Operators for Proving Termination by Abstract Interpretation. In TACAS, 2017.

PDF Code Project Slides BibTeX Springer FuncTion

. Inference of Ranking Functions for Proving Temporal Properties by Abstract Interpretation. In COMLAN, 2017.

PDF Code Project BibTeX HAL Elsevier FuncTion

. Static Analysis by Abstract Interpretation of Functional Temporal Properties of Programs. PhD Thesis, 2015.

PDF Code Project Slides BibTeX HAL FuncTion

. FuncTion: An Abstract Domain Functor for Termination (Competition Contribution). In TACAS, 2015.

PDF Code Project BibTeX HAL Springer FuncTion

. Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation. In VMCAI, 2015.

PDF Code Project Slides BibTeX HAL Springer FuncTion

. A Decision Tree Abstract Domain for Proving Conditional Termination. In SAS, 2014.

PDF Code Project Slides BibTeX HAL Springer FuncTion

. To Infinity... and Beyond!. In WST, 2014.

PDF Code Project Slides BibTeX HAL FuncTion

. An Abstract Domain to Infer Ordinal-Valued Ranking Functions. In ESOP, 2014.

PDF Code Project Slides BibTeX HAL Springer FuncTion

. Piecewise-Defined Ranking Functions. In WST, 2013.

Code Project FuncTion

. The Abstract Domain of Segmented Ranking Functions. In SAS, 2013.

PDF Code Project Slides BibTeX HAL Springer FuncTion

Talks

Bringing Abstract Interpretation To Termination And Beyond
Thursday, May 19, 2016
Dagstuhl Seminar 16201 “Synergies among Testing, Verification, and Repair for Concurrent Programs”, 🇩🇪 Schloss Dagstuhl, Germany
Project
🇫🇷 Analyse Statique par Interprétation Abstraite de Propriétés Temporelles des Programmes
Thursday, January 28, 2016 8:45 AM
Congrès SIF 2016, 🇫🇷 Strasbourg, France
Project
Counterexample-Guided Inference of Ranking Functions
Thursday, July 30, 2015 3:30 PM
🇺🇸 SRI International, USA
Project
Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation
Thursday, December 18, 2014 10:30 AM
🇮🇹 Università degli Studi di Udine, Italy
Project
Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation
Monday, November 3, 2014 10:30 AM
🇨🇭 ETH Zurich, Switzerland
Project
Automatic Inference of Ranking Functions by Abstract Interpretation
Wednesday, October 1, 2014 11:00 AM
Theory Group Seminar, 🇬🇧 Queen Mary University of London, UK
Project
Automatic Inference of Ranking Functions by Abstract Interpretation
Tuesday, August 26, 2014
Dagstuhl Seminar 14352 “Next Generation Static Software Analysis Tools”, 🇩🇪 Schloss Dagstuhl, Germany
Slides Project
Automatic Inference of Ranking Functions by Abstract Interpretation
Wednesday, June 18, 2014 4:00 PM
🇬🇧 University College London, UK
Project
An Abstract Domain to Infer Ordinal-Valued Ranking Functions
Wednesday, May 28, 2014 2:30 PM
Séminaire 68NQRT, 🇫🇷 INRIA Rennes, France
Project
Automatic Inference of Ranking Functions by Abstract Interpretation
Tuesday, March 18, 2014 2:00 PM
INRIA Junior Seminar, 🇫🇷 INRIA Paris-Rocquencourt, France
Slides Video Project
Automatic Inference of Ranking Functions by Abstract Interpretation
Thursday, January 16, 2014 11:00 AM
🇺🇸 IBM Thomas J. Watson Research Center, USA
Project
The Abstract Domain of Piecewise-Defined Ranking Functions
Thursday, November 28, 2013 3:00 PM
🇨🇳 East China Normal University, China
Slides Project
The Abstract Domain of Piecewise-Defined Ranking Functions
Saturday, November 23, 2013 2:00 PM
2nd Workshop on Analysis and Verification of Dependable Cyber Physical Software (AVDCPS 2013), 🇨🇳 National University of Defense Technology, China
Slides Project
The Abstract Domain of Segmented Ranking Functions
Monday, March 25, 2013 11:30 AM
🇮🇹 Università degli Studi di Udine, Italy
Project