ALICe documentation


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



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.


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.


Program termination analysis in polynomial time

By: Amir M Ben-Amram, Chin Soon Lee.

In: ACM Trans. Program. Lang. Syst., 2007.

Model: ackerman.


Invariant Synthesis for Combined Theories

By: Dirk Beyer, Thomas A Henzinger, Rupak Majumdar, Andrey Rybalchenko.

In: VMCAI, 2007.

Models: disj, forward.


Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic

By: Tevfik Bultan, Richard Gerber, William Pugh.

In: CAV, 1997.

Models: bakery, ticket.


Ranking Abstractions

By: Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang.

In: ESOP, 2008.

Models: aaron2, easy1, easy2, random1d, random2d, sipmabubble.


Synthesis of Linear Ranking Functions

By: Michael Colón, Henny Sipma.

In: TACAS, 2001.

Model: terminate.


Practical Methods for Proving Program Termination

By: Michael Colón, Henny Sipma.

In: CAV, 2002.

Model: maccarthy91.


Termination proofs for systems code

By: Byron Cook, Andreas Podelski, Andrey Rybalchenko.

In: PLDI, 2006.

Model: terminator.


Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming

By: Patrick Cousot.

In: VMCAI, 2005.

Model: cousot9.


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.


Lookahead Widening

By: Denis Gopan, Thomas W Reps.

In: CAV, 2006.

Models: gopan_reps, gopan_reps_alt1, gopan_reps_alt2.


Guided Static Analysis

By: Denis Gopan, Thomas W Reps.

In: SAS, 2007.

Models: gopan_reps, gopan_reps_alt1, gopan_reps_alt2, speedometer.


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.


SPEED: Symbolic Complexity Bound Analysis

By: Sumit Gulwani.

In: CAV, 2009.

Models: gulwani1, gulwani1_alt, gulwani2, gulwani2_alt, gulwani3.


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.


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.


The reachability-bound problem

By: Sumit Gulwani, Florian Zuleger.

In: PLDI, 2010.

Models: disj, gopan_reps, microsoftex2, microsoftex4, microsoftex5, microsoftex6, microsoftex7, popeea, slam.


Delay Analysis in Synchronous Programs

By: Nicolas Halbwachs.

In: CAV, 1993.

Models: car, metro, subway.


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.


Linear Relation Analysis: Principles and Recent Progress

By: Nicolas Halbwachs.

Presentation at Second French Compiler Research Meeting, 2010.

Models: halbwachs3, halbwachs4, halbwachs5, halbwachs6, halbwachs7.


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.


Static Analysis by Abstract Interpretation, Path Focusing

By: Julien Henry.

Presentation at Third GDR GPL Meeting, 2011.

Model: henry.


Lazy abstraction

By: Thomas A Henzinger, Ranjit Jhala, Rupak Majumdar, Grégoire Sutre.

In: POPL, 2002.

Model: slam.


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.


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.


Réduction du nombre de variables en analyse de relations linéaires

By: David Merchat.

At: Université Joseph-Fourier - Grenoble I, 2005.

Model: car.


A Complete Method for the Synthesis of Linear Ranking Functions

By: Andreas Podelski, Andrey Rybalchenko.

In: VMCAI, 2004.

Model: loops.


Inferring Disjunctive Postconditions

By: Corneliu Popeea, Wei-Ngan Chin.

In: ASIAN, 2006.

Model: popeea.

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