Delay analysis in synchronous programs
Lecture notes in computer sciencePublished 1 January 1993
Nicolas Halbwachs
Citations135
SJR quartileQ2
SJR score0.35
SNIP0.55
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
This work proposes to apply linear relation analysis to variables used to count delays in synchronous programs, and finds that the results can be applied to code optimization and to the verification of real-time properties of programs.
Abstract
Linear relation analysis [CH78, Hal79] has been proposed a long time ago as an abstract interpretation which permits to discover linear relations invariantly satisfied by the variables of a program. Here, we propose to apply this general method to variables used to count delays in synchronous programs. The "regular" behavior of these counters makes the results of the analysis especially precise. These results can be applied to code optimization and to the verification of real-time properties of programs.
Keywords
Computer Science
Abstract interpretation
6,131 Citations1977Patrick Cousot, Radhia Cousot
Automatic discovery of linear restraints among variables of a program
1,576 Citations1978Patrick Cousot, Nicolas Halbwachs
Model-checking for real-time systems
890 Citations2002Rajeev Alur, Costas Courcoubetis +1 more
An algorithm is developed for model checking, that is, for determining the truth of a TCTL formula with respect to a timed graph, and it is argued that choosing a dense domain, instead of a discrete domain, to model time does not blow up the complexity of the model-checking problem.
The Journal of Logic ProgrammingAbstract interpretation and application to logic programs
585 Citations1992Patrick Cousot, Radhia Cousot
This classical formal framework for abstract interpretation of programs can be applied in extenso to logic programs and is recalled, using a variant of SLD-resolution as the ground operational semantics.
Proceedings of the IEEEThe ESTEREL language
442 Citations1991Frédéric Boussinot, Rosaria Simone
The authors present the basics of the ESTEREL reactive model of synchronous parallel systems, based on instantaneous communications and decisions, and it is shown how programs can be compiled into finite state sequential machines for efficient execution.
Lecture notes in computer scienceComparing the Galois connection and widening/narrowing approaches to abstract interpretation
421 Citations2006Patrick Cousot, Radhia Cousot
The use of infinite abstract domains with widening and narrowing for accelerating the convergence of abstract interpretations is shown to be more powerful than the Galois connection approach restricted to finite lattices.
Protocol verification as a hardware design aid
399 Citations2003David L. Dill, Andreas J. Drexler +2 more
Techniques for automatic verification of real-time systems
175 Citations1992Rajeev Alur
The distinguishing feature of this work is the use of the set of reals to model time; it is argued that the denseness of the time domain is crucial for modeling event-driven asynchronous systems.
A Note on Chernikova's algorithm
120 Citations1992Hervé Le Verge
An implementation of Chernikova's algorithm for finding an irredundant set of vertices for a given polyhedron defined by a set of linear inequalities and equations based on the polyhedral cone duality principle is described.
USSR Computational Mathematics and Mathematical PhysicsAlgorithm for discovering the set of all the solutions of a linear programming problem
75 Citations1968N.V. Chernikoba
HAL (Le Centre pour la Communication Scientifique Directe)Détermination automatique de relations linéaires vérifiées par les variables d'un programme
61 Citations1979Nicolas Halbwachs
Systeme d'equations en avant associe a un programme, definitions and resultats fondamentaux sur les polyedres convexes, applications de la methode, anders avec des travaux voisins.
Acta InformaticaAn experience in proving regular networks of processes by modular model checking
34 Citations1992Nicolas Halbwachs, F. Lagnier +1 more
This paper presents a complete example of the use of the synchronous declarative language LUSTRE for the specification, description and verification of a resource arbiter, which is a regular network of hardware devices.
Lecture notes in computer scienceVerifying quantitative real-time properties of synchronous programs
28 Citations1993Muriel Jourdan, Florence Maraninchi +1 more
The Argos language is extended with a single delay construct that allows to express watchdogs and timeouts, at any level in the parallel or hierarchic structure of a program, and the semantics are defined in terms of Timed Graphs, showing that it is a “convenient” extension of the pure Argos synchronous semantics.
Design verification and reachability analysis using algebraic manipulation
25 Citations2002Srinivas Devadas, Kurt Keutzer +1 more
Design verification is the process of checking that the specification of a circuit satisfies certain correctness properties, using temporal logic and model checking, as well as the use of higher-order logic and theorem proving.
IEEE/ACM International Conference on Computer-Aided DesignVerification of systems containing counters
15 Citations1992Macii, Plessier +1 more
It is pointed out that systems containing counters have very large and deep state spaces, and the verification of properties on these systems can be very expensive in terms of memory space and computation time.
Lecture notes in computer scienceVerifying general safety and liveness properties with integer programming
12 Citations1993James C. Corbett
This work extends the constrained expression analysis technique to the verification of more complex safety properties that involve the order of events and to the verify of liveness properties, which involve infinite executions.