Correct Hardware Design and Verification Methods
Lecture notes in computer sciencePublished 1 January 1999
Marius Bozga, Oded Maler
Citations377
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.
Abstract
CHARME'99 is the tenth in a series of working conferences devoted to the dev- opment and use of leading-edge formal techniques and tools for the design and veri?cation of hardware and systems. Previou
Keywords
Computer Science
Lecture notes in computer scienceWhat good are digital clocks?
276 Citations1992Thomas A. Henzinger, Zohar Manna +1 more
What can the authors conclude if a real-time system has been shown “correct” for integral observations?
Lecture notes in computer scienceModel checking of real-time reachability properties using abstractions
187 Citations1998Conrado Daws, Stavros Tripakis
This work proposes to use abstractions reducing the state-space while preserving reachability properties to cope with state explosion, and has permitted to verify two benchmark examples with a significant scale-up in size.
Texts and monographs in computer scienceAsynchronous Circuits
169 Citations1995Janusz Brzozowski, Carl-Johan H. Seger
The asynchronous circuits is one book that the authors really recommend you to read, to get more solutions in solving this problem.
Reducing the number of clock variables of timed automata
136 Citations2002Conrado Daws, Sergio Yovine
Experimental results show that an appropriate encoding of the state space, based on the output of the algorithms, leads to a considerable reduction of the memory space allowing a more eficient Verification.
Lecture notes in computer scienceDelay analysis in synchronous programs
135 Citations1993Nicolas Halbwachs
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.
Lecture notes in computer scienceTiming analysis of asynchronous circuits using timed automata
91 Citations1995Oded Maler, Amir Pnueli
These results, combined with recent results concerning the analysis and synthesis of timed automata, provide for the systematic Treatment of a large class of problems that could be treated by conventional simulation methods only in an ad-hoc fashion.
Lecture notes in computer scienceTiming analysis in COSPAN
90 Citations1996Rajeev Alur, Robert P. Kurshan
This work describes how to model and verify real-time systems using the formal verification tool Cospan, which supports automata-theoretic verification of coordinating processes with timing constraints.
Lecture notes in computer scienceVerifying abstractions of timed systems
89 Citations1996Serdar Taşiran, Rajeev Alur +2 more
A compositional framework for the implementation check to be carried out in a module-by-module manner using assume-guarantee style proof rules is developed and it is shown that the problem of checking the existence of timed simulation relations, a sufficient condition for correct implementation, is decidable.
Branching time and abstraction in bisimulation semantics
82 Citations1989R.J. vanGlabbeek, W. P. Weijland
Lecture notes in computer scienceOn discretization of delays in timed automata and digital circuits
70 Citations1998Eugène Asarin, Oded Maler +1 more
Approximate reachability analysis of timed automata
64 Citations2002Felice Balarin
Two algorithms for computing a superset of reachable states of a timed automaton involve only manipulation of Boolean functions, which are competitive with the best published results, but that further improvements are necessary to scale up to realistic systems.
Lecture notes in computer scienceSymbolic equivalence checking
39 Citations1993J. C. Fernandez, A. Kerbrat +1 more
The implementation, within Aldebaran of an algorithmic method allowing the generation of a minimal labeled transition system from an abstract model; this minimality is relative to an equivalence relation.
Lecture notes in computer scienceMinimizable timed automata
35 Citations1996Jan Springintveld, Frits Vaandrager
This chapter discusses algorithms and results based on the fact that for each finite automaton there exists an equivalent minimum state automaton that can be effectively computed and that is unique up to isomorphism.