ALICe documentation

Bibliography

«  List of tags   ::   Contents   ::   Model aaron2  »

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.

Models: disj, forward.

[BultanGP97]

Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic

By: Tevfik Bultan, Richard Gerber, William Pugh.

In: CAV, 1997.

Models: bakery, ticket.

[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.

[Halbwachs93]

Delay Analysis in Synchronous Programs

By: Nicolas Halbwachs.

In: CAV, 1993.

Models: car, metro, subway.

[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.

[PodelskiR04]

A Complete Method for the Synthesis of Linear Ranking Functions

By: Andreas Podelski, Andrey Rybalchenko.

In: VMCAI, 2004.

Model: loops.

[PopeeaC06]

Inferring Disjunctive Postconditions

By: Corneliu Popeea, Wei-Ngan Chin.

In: ASIAN, 2006.

Model: popeea.

«  List of tags   ::   Contents   ::   Model aaron2  »