Bibliography¶
[AliasDFG10]¶
Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
By: Christophe Alias, Alain Darte, Paul Feautrier, Laure Gonnord.
In: SAS, 2010.
Models: ax, counterex1, determinant, exmini, gcd, insertsort, nd_loop, ndecr, perfect, realbubble, realheapsort, realheapsort_step1, realheapsort_step2, realselect, realshellsort, relation1, rsd, wcet1, wcet2, while2, wise.
[Bardin_thesis]¶
Vers un Model Checking avec accélération plate des systèmes hétérogènes
By: Sébastien Bardin.
At: École normale supérieure de Cachan - ENS Cachan, 2005.
Model: bardin.
[BenAmramL07]¶
Program termination analysis in polynomial time
By: Amir M Ben-Amram, Chin Soon Lee.
In: ACM Trans. Program. Lang. Syst., 2007.
Model: ackerman.
[BeyerHMR07]¶
Invariant Synthesis for Combined Theories
By: Dirk Beyer, Thomas A Henzinger, Rupak Majumdar, Andrey Rybalchenko.
In: VMCAI, 2007.
[BultanGP97]¶
Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic
By: Tevfik Bultan, Richard Gerber, William Pugh.
In: CAV, 1997.
[ChawdharyCGSY08]¶
Ranking Abstractions
By: Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang.
In: ESOP, 2008.
Models: aaron2, easy1, easy2, random1d, random2d, sipmabubble.
[ColonS01]¶
Synthesis of Linear Ranking Functions
By: Michael Colón, Henny Sipma.
In: TACAS, 2001.
Model: terminate.
[ColonS02]¶
Practical Methods for Proving Program Termination
By: Michael Colón, Henny Sipma.
In: CAV, 2002.
Model: maccarthy91.
[CookPR06]¶
Termination proofs for systems code
By: Byron Cook, Andreas Podelski, Andrey Rybalchenko.
In: PLDI, 2006.
Model: terminator.
[Cousot05]¶
Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming
By: Patrick Cousot.
In: VMCAI, 2005.
Model: cousot9.
[Gonnord_thesis]¶
Accélération abstraite pour l’amélioration de la précision en Analyse des Relations Linéaires
By: Laure Gonnord.
At: Université Joseph-Fourier - Grenoble I, 2007.
Models: bardin, car, car_simple, gasburner, gasburner_alt, gonnord1, gonnord2, gonnord3, gonnord4, gonnord5, gonnord6, halbwachs1, halbwachs2.
[GopanR06]¶
Lookahead Widening
By: Denis Gopan, Thomas W Reps.
In: CAV, 2006.
Models: gopan_reps, gopan_reps_alt1, gopan_reps_alt2.
[GopanR07]¶
Guided Static Analysis
By: Denis Gopan, Thomas W Reps.
In: SAS, 2007.
Models: gopan_reps, gopan_reps_alt1, gopan_reps_alt2, speedometer.
[GulavaniHKNR06]¶
SYNERGY: a new algorithm for property checking
By: Bhargav S Gulavani, Thomas A Henzinger, Yamini Kannan, Aditya V Nori, Sriram K Rajamani.
In: SIGSOFT FSE, 2006.
Models: leeyannakis_bad, slam, slam_bad, synergy_bad.
[Gulwani09]¶
SPEED: Symbolic Complexity Bound Analysis
By: Sumit Gulwani.
In: CAV, 2009.
Models: gulwani1, gulwani1_alt, gulwani2, gulwani2_alt, gulwani3.
[GulwaniJK09]¶
Control-flow refinement and progress invariants for bound analysis
By: Sumit Gulwani, Sagar Jain, Eric Koskinen.
In: PLDI, 2009.
Models: gopan_reps, gulwani4, interleaving1, interleaving2, interleaving3, interleaving4, nested, slam.
[GulwaniMC09]¶
SPEED: precise and efficient static estimation of program computational complexity
By: Sumit Gulwani, Krishna K Mehra, Trishul M Chilimbi.
In: POPL, 2009.
Models: counters1, counters2, counters3, counters4, disjbnd1, disjbnd2, multcounters1, multcounters2, multcounters3, multcounters4.
[GulwaniZ10]¶
The reachability-bound problem
By: Sumit Gulwani, Florian Zuleger.
In: PLDI, 2010.
Models: disj, gopan_reps, microsoftex2, microsoftex4, microsoftex5, microsoftex6, microsoftex7, popeea, slam.
[HalbwachsPR97]¶
Verification of Real-Time Systems using Linear Relation Analysis
By: Nicolas Halbwachs, Yann-Erick Proy, Patrick Roumanoff.
In: Formal Methods in System Design, 1997.
Models: car, car_simple, metro, subway.
[Halbwachs_misc10]¶
Linear Relation Analysis: Principles and Recent Progress
By: Nicolas Halbwachs.
Presentation at Second French Compiler Research Meeting, 2010.
Models: halbwachs3, halbwachs4, halbwachs5, halbwachs6, halbwachs7.
[Halbwachs_thesis]¶
Détermination automatique de relations linéaires vérifiées par les variables d’un programme
By: Nicolas Halbwachs.
At: Institut National Polytechnique de Grenoble - INPG; Université Joseph-Fourier - Grenoble I, 1978.
Models: car, halbwachs1, halbwachs2, halbwachs8, halbwachs9.
[Henry_misc11]¶
Static Analysis by Abstract Interpretation, Path Focusing
By: Julien Henry.
Presentation at Third GDR GPL Meeting, 2011.
Model: henry.
[HenzingerJMS02]¶
Lazy abstraction
By: Thomas A Henzinger, Ranjit Jhala, Rupak Majumdar, Grégoire Sutre.
In: POPL, 2002.
Model: slam.
[Jeannet_thesis]¶
Partitionnement dynamique dans l’analyse de relations linéaires et application à la vérification de programmes synchrones
By: Bertrand Jeannet.
At: Institut National Polytechnique Grenoble, 2000.
Models: jeannet1, jeannet2, jeannet3, jeannet4, jeannet5, jeannet6.
[KatzEWPS85]¶
Implementing A Cache Consistency Protocol
By: Randy H Katz, Susan J Eggers, David A Wood, C L Perkins, R G Sheldon.
In: ISCA, 1985.
Model: berkeley.
[Merchat_thesis]¶
Réduction du nombre de variables en analyse de relations linéaires
By: David Merchat.
At: Université Joseph-Fourier - Grenoble I, 2005.
Model: car.