---
_id: '4566'
abstract:
- lang: eng
text: "Complex system design today calls for compositional design and implementation.
However each component is designed with certain assumptions about the environment
it is meant to operate in, and delivering certain guarantees if those assumptions
are satisfied; numerous inter-component interaction errors are introduced in the
manual and error-prone integration process as there is little support in design
environments for machine-readably representing these assumptions and guarantees
and automatically checking consistency during integration.\r\n\r\nBased on Interface
Automata we propose a framework for compositional design and analysis of systems:
a set of domain-specific automata-theoretic type systems for compositional system
specification and analysis by behavioral specification of open systems. We focus
on three different domains: component-based hardware systems communicating on
bidirectional wires. concurrent distributed recursive message-passing software
systems, and embedded software system components operating in resource-constrained
environments. For these domains we present approaches to formally represent the
assumptions and conditional guarantees between interacting open system components.
Composition of such components produces new components with the appropriate assumptions
and guarantees. We check satisfaction of temporal logic specifications by such
components, and the substitutability of one component with another in an arbitrary
context. Using this framework one can analyze large systems incrementally without
needing extensive summary information to close the system at each stage. Furthermore,
we focus only on the inter-component interaction behavior without dealing with
the full implementation details of each component. Many of the merits of automata-theoretic
model-checking are combined with the compositionality afforded by type-system
based techniques. We also present an integer-based extension of the conventional
boolean verification framework motivated by our interface formalism for embedded
software components.\r\n\r\nOur algorithms for checking the behavioral compatibility
of component interfaces are available in our tool Chic, which can be used as a
plug-in for the Java IDE JBuilder and the heterogenous modeling and design environment
Ptolemy II.\r\n\r\nFinally, we address the complementary problem of partitioning
a large system into meaningful coherent components by analyzing the interaction
patterns between its basic elements. We demonstrate the usefulness of our partitioning
approach by evaluating its efficacy in improving unit-test branch coverage for
a large software system implemented in C."
article_processing_charge: No
author:
- first_name: Arindam
full_name: Chakrabarti, Arindam
last_name: Chakrabarti
citation:
ama: Chakrabarti A. A framework for compositional design and analysis of systems.
2007:1-244.
apa: Chakrabarti, A. (2007). *A framework for compositional design and analysis
of systems*. University of California, Berkeley.
chicago: Chakrabarti, Arindam. “A Framework for Compositional Design and Analysis
of Systems.” University of California, Berkeley, 2007.
ieee: A. Chakrabarti, “A framework for compositional design and analysis of systems,”
University of California, Berkeley, 2007.
ista: Chakrabarti A. 2007. A framework for compositional design and analysis of
systems. University of California, Berkeley.
mla: Chakrabarti, Arindam. *A Framework for Compositional Design and Analysis
of Systems*. University of California, Berkeley, 2007, pp. 1–244.
short: A. Chakrabarti, A Framework for Compositional Design and Analysis of Systems,
University of California, Berkeley, 2007.
date_created: 2018-12-11T12:09:31Z
date_published: 2007-12-20T00:00:00Z
date_updated: 2021-01-12T07:59:45Z
day: '20'
extern: '1'
language:
- iso: eng
month: '12'
oa_version: None
page: 1 - 244
publication_status: published
publisher: University of California, Berkeley
publist_id: '145'
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: George
full_name: Necula, George
last_name: Necula
- first_name: Edward
full_name: Lee, Edward
last_name: Lee
- first_name: Jack
full_name: Silver, Jack
last_name: Silver
title: A framework for compositional design and analysis of systems
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2007'
...
---
_id: '4236'
article_processing_charge: No
author:
- first_name: Harold
full_name: de Vladar, Harold
id: 2A181218-F248-11E8-B48F-1D18A9856A87
last_name: de Vladar
orcid: 0000-0002-5985-7653
citation:
ama: de Vladar H. Métodos no lineales y sus aplicaciones en dinámicas aleatorias
de poblaciones celulares. 2004. doi:3810
apa: de Vladar, H. (2004). *Métodos no lineales y sus aplicaciones en dinámicas
aleatorias de poblaciones celulares*. Centro de estudios avazados, IVIC. https://doi.org/3810
chicago: Vladar, Harold de. “Métodos No Lineales y Sus Aplicaciones En Dinámicas
Aleatorias de Poblaciones Celulares.” Centro de estudios avazados, IVIC, 2004.
https://doi.org/3810.
ieee: H. de Vladar, “Métodos no lineales y sus aplicaciones en dinámicas aleatorias
de poblaciones celulares,” Centro de estudios avazados, IVIC, 2004.
ista: de Vladar H. 2004. Métodos no lineales y sus aplicaciones en dinámicas aleatorias
de poblaciones celulares. Centro de estudios avazados, IVIC.
mla: de Vladar, Harold. *Métodos No Lineales y Sus Aplicaciones En Dinámicas Aleatorias
de Poblaciones Celulares*. Centro de estudios avazados, IVIC, 2004, doi:3810.
short: H. de Vladar, Métodos No Lineales y Sus Aplicaciones En Dinámicas Aleatorias
de Poblaciones Celulares, Centro de estudios avazados, IVIC, 2004.
date_created: 2018-12-11T12:07:46Z
date_published: 2004-01-01T00:00:00Z
date_updated: 2021-01-12T07:55:30Z
day: '01'
doi: '3810'
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
publication_status: published
publisher: Centro de estudios avazados, IVIC
publist_id: '1877'
status: public
title: Métodos no lineales y sus aplicaciones en dinámicas aleatorias de poblaciones
celulares
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2004'
...
---
_id: '4424'
abstract:
- lang: eng
text: "The enormous cost and ubiquity of software errors necessitates the need for
techniques and tools that can precisely analyze large systems and prove that they
meet given specifications, or if they don't, return counterexample behaviors showing
how the system fails. Recent advances in model checking, decision procedures,
program analysis and type systems, and a shift of focus to partial specifications
common to several systems (e.g., memory safety and race freedom) have resulted
in several practical verification methods. However, these methods are either precise
or they are scalable, depending on whether they track the values of variables
or only a fixed small set of dataflow facts (e.g., types), and are usually insufficient
for precisely verifying large programs.\r\n\r\nWe describe a new technique called
Lazy Abstraction (LA) which achieves both precision and scalability by localizing
the use of precise information. LA automatically builds, explores and refines
a single abstract model of the program in a way that different parts of the model
exhibit different degrees of precision, namely just enough to verify the desired
property. The algorithm automatically mines the information required by partitioning
mechanical proofs of unsatisfiability of spurious counterexamples into Craig Interpolants.
For multithreaded systems, we give a new technique based on analyzing the behavior
of a single thread executing in a context which is an abstraction of the other
(arbitrarily many) threads. We define novel context models and show how to automatically
infer them and analyze the full system (thread + context) using LA.\r\n\r\nLA
is implemented in BLAST. We have run BLAST on Windows and Linux Device Drivers
to verify API conformance properties, and have used it to find (or guarantee the
absence of) data races in multithreaded Networked Embedded Systems (NESC) applications.
BLAST is able to prove the absence of races in several cases where earlier methods,
which depend on lock-based synchronization, fail."
article_processing_charge: No
author:
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
citation:
ama: Jhala R. Program verification by lazy abstraction. 2004:1-165.
apa: Jhala, R. (2004). *Program verification by lazy abstraction*. University
of California, Berkeley.
chicago: Jhala, Ranjit. “Program Verification by Lazy Abstraction.” University of
California, Berkeley, 2004.
ieee: R. Jhala, “Program verification by lazy abstraction,” University of California,
Berkeley, 2004.
ista: Jhala R. 2004. Program verification by lazy abstraction. University of California,
Berkeley.
mla: Jhala, Ranjit. *Program Verification by Lazy Abstraction*. University
of California, Berkeley, 2004, pp. 1–165.
short: R. Jhala, Program Verification by Lazy Abstraction, University of California,
Berkeley, 2004.
date_created: 2018-12-11T12:08:47Z
date_published: 2004-12-01T00:00:00Z
date_updated: 2021-01-12T07:56:52Z
day: '01'
extern: '1'
language:
- iso: eng
month: '12'
oa_version: None
page: 1 - 165
publication_status: published
publisher: University of California, Berkeley
publist_id: '307'
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: Program verification by lazy abstraction
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2004'
...
---
_id: '2414'
author:
- first_name: Uli
full_name: Uli Wagner
id: 36690CA2-F248-11E8-B48F-1D18A9856A87
last_name: Wagner
orcid: 0000-0002-1494-0568
citation:
ama: Wagner U. On k-Sets and Their Applications. 2003. doi:10.3929/ethz-a-004708408
apa: Wagner, U. (2003). *On k-Sets and Their Applications*. ETH Zurich. https://doi.org/10.3929/ethz-a-004708408
chicago: Wagner, Uli. “On K-Sets and Their Applications.” ETH Zurich, 2003. https://doi.org/10.3929/ethz-a-004708408.
ieee: U. Wagner, “On k-Sets and Their Applications,” ETH Zurich, 2003.
ista: Wagner U. 2003. On k-Sets and Their Applications. ETH Zurich.
mla: Wagner, Uli. *On K-Sets and Their Applications*. ETH Zurich, 2003, doi:10.3929/ethz-a-004708408.
short: U. Wagner, On K-Sets and Their Applications, ETH Zurich, 2003.
date_created: 2018-12-11T11:57:31Z
date_published: 2003-01-01T00:00:00Z
date_updated: 2021-01-12T06:57:20Z
day: '01'
doi: 10.3929/ethz-a-004708408
extern: 1
month: '01'
publication_status: published
publisher: ETH Zurich
publist_id: '4511'
quality_controlled: 0
status: public
title: On k-Sets and Their Applications
type: dissertation
year: '2003'
...
---
_id: '4416'
abstract:
- lang: eng
text: "Methods for the formal specification and verification of systems are indispensible
for the development of complex yet correct systems. In formal verification, the
designer describes the system in a modeling language with a well-defined semantics,
and this system description is analyzed against a set of correctness requirements.
Model checking is an algorithmic technique to check that a system description
indeed satisfies correctness requirements given as logical specifications. While
successful in hardware verification, the potential for model checking for software
and embedded systems has not yet been realized. This is because traditional model
checking focuses on systems modeled as finite state-transition graphs. While a
natural model for hardware (especially synchronous hardware), state-transition
graphs often do not capture software and embedded systems at an appropriate level
of granularity. This dissertation considers two orthogonal extensions to finite
state-transition graphs making model checking techniques applicable to both a
wider class of systems and a wider class of properties.\r\n\r\nThe first direction
is an extension to infinite-state structures finitely represented using constraints
and operations on constraints. Infinite state arises when we wish to model variables
with unbounded range (e.g., integers), or data structures, or real time. We provide
a uniform framework of symbolic region algebras to study model checking of infinite-state
systems. We also provide sufficient language-independent termination conditions
for symbolic model checking algorithms on infinite state systems.\r\n\r\nThe second
direction supplements verification with game theoretic reasoning. Games are natural
models for interactions between components. We study game theoretic behavior with
winning conditions given by temporal logic objectives both in the deterministic
and in the probabilistic context. For deterministic games, we provide an extremal
model characterization of fixpoint algorithms that link solutions of verification
problems to solutions for games. For probabilistic games we study fixpoint characterization
of winning probabilities for games with omega-regular winning objectives, and
construct (epsilon-)optimal winning strategies."
article_processing_charge: No
author:
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: Majumdar R. Symbolic algorithms for verification and control. 2003:1-201.
apa: Majumdar, R. (2003). *Symbolic algorithms for verification and control*.
University of California, Berkeley.
chicago: Majumdar, Ritankar. “Symbolic Algorithms for Verification and Control.”
University of California, Berkeley, 2003.
ieee: R. Majumdar, “Symbolic algorithms for verification and control,” University
of California, Berkeley, 2003.
ista: Majumdar R. 2003. Symbolic algorithms for verification and control. University
of California, Berkeley.
mla: Majumdar, Ritankar. *Symbolic Algorithms for Verification and Control*.
University of California, Berkeley, 2003, pp. 1–201.
short: R. Majumdar, Symbolic Algorithms for Verification and Control, University
of California, Berkeley, 2003.
date_created: 2018-12-11T12:08:44Z
date_published: 2003-12-01T00:00:00Z
date_updated: 2021-01-12T07:56:49Z
day: '01'
extern: '1'
language:
- iso: eng
month: '12'
oa_version: None
page: 1 - 201
publication_status: published
publisher: University of California, Berkeley
publist_id: '313'
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: Symbolic algorithms for verification and control
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2003'
...
---
_id: '4425'
abstract:
- lang: eng
text: "Giotto provides a time-triggered programmer’s model for the implementation
of embedded control systems with hard real-time constraints. Giotto’s precise
semantics and predictabil- ity make it suitable for safety-critical applications.\r\nGiotto
is based around the idea that time-triggered task invocation together with time-triggered
mode switching can form a useful programming model for real-time systems. To substantiate
this claim, we describe the use of Giotto to refactor the software of a small,
autonomous helicopter. The ease with which Giotto expresses the existing software
provides evidence that Giotto is an appropriate programming language for control
systems.\r\nSince Giotto is a real-time programming language, ensuring that Giotto
programs meet their deadlines is crucial. To study precedence-constrained Giotto
scheduling, we first examine single-mode, single-processor scheduling. We extend
to an infinite, periodic setting the classical problem of meeting deadlines for
a set of tasks with release times, deadlines, precedence constraints, and preemption.
We then develop an algorithm for scheduling Giotto programs on a single processor
by representing Giotto programs as instances of the extended scheduling problem.\r\nNext,
we study multi-mode, single-processor Giotto scheduling. This problem is different
from classical scheduling problems, since in our precedence-constrained approach,
the deadlines of tasks may vary depending on the mode switching behavior of the
program. We present conditional scheduling models which capture this varying-deadline
behavior. We develop polynomial-time algorithms for some conditional scheduling
models, and prove oth- ers to be computationally hard. We show how to represent
multi-mode Giotto programs as instances of the model, resulting in an algorithm
for scheduling multi-mode Giotto programs on a single processor.\r\nFinally, we
show that the problem of scheduling Giotto programs for multiple net- worked processors
is strongly NP-hard."
article_processing_charge: No
author:
- first_name: Benjamin
full_name: Horowitz, Benjamin
last_name: Horowitz
citation:
ama: 'Horowitz B. Giotto: A time-triggered language for embedded programming. 2003:1-237.'
apa: 'Horowitz, B. (2003). *Giotto: A time-triggered language for embedded programming*.
University of California, Berkeley.'
chicago: 'Horowitz, Benjamin. “Giotto: A Time-Triggered Language for Embedded Programming.”
University of California, Berkeley, 2003.'
ieee: 'B. Horowitz, “Giotto: A time-triggered language for embedded programming,”
University of California, Berkeley, 2003.'
ista: 'Horowitz B. 2003. Giotto: A time-triggered language for embedded programming.
University of California, Berkeley.'
mla: 'Horowitz, Benjamin. *Giotto: A Time-Triggered Language for Embedded Programming*.
University of California, Berkeley, 2003, pp. 1–237.'
short: 'B. Horowitz, Giotto: A Time-Triggered Language for Embedded Programming,
University of California, Berkeley, 2003.'
date_created: 2018-12-11T12:08:47Z
date_published: 2003-10-01T00:00:00Z
date_updated: 2021-01-12T07:56:53Z
day: '01'
extern: '1'
language:
- iso: eng
month: '10'
oa_version: None
page: 1 - 237
publication_status: published
publisher: University of California, Berkeley
publist_id: '305'
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: 'Giotto: A time-triggered language for embedded programming'
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2003'
...
---
_id: '3678'
author:
- first_name: Christoph
full_name: Christoph Lampert
id: 40C20FD2-F248-11E8-B48F-1D18A9856A87
last_name: Lampert
orcid: 0000-0001-8622-7887
citation:
ama: Lampert C. The Neumann operator in strictly pseudoconvex domains with weighted
Bergman metric . *Bonner Mathematische Schriften*. 2003;356:1-165.
apa: Lampert, C. (2003). *The Neumann operator in strictly pseudoconvex domains
with weighted Bergman metric *. *Bonner Mathematische Schriften*. Universität
Bonn, Fachbibliothek Mathematik.
chicago: Lampert, Christoph. “The Neumann Operator in Strictly Pseudoconvex Domains
with Weighted Bergman Metric .” *Bonner Mathematische Schriften*. Universität
Bonn, Fachbibliothek Mathematik, 2003.
ieee: C. Lampert, “The Neumann operator in strictly pseudoconvex domains with weighted
Bergman metric ,” Universität Bonn, Fachbibliothek Mathematik, 2003.
ista: Lampert C. 2003. The Neumann operator in strictly pseudoconvex domains with
weighted Bergman metric . Universität Bonn, Fachbibliothek Mathematik.
mla: Lampert, Christoph. “The Neumann Operator in Strictly Pseudoconvex Domains
with Weighted Bergman Metric .” *Bonner Mathematische Schriften*, vol. 356,
Universität Bonn, Fachbibliothek Mathematik, 2003, pp. 1–165.
short: C. Lampert, The Neumann Operator in Strictly Pseudoconvex Domains with Weighted
Bergman Metric , Universität Bonn, Fachbibliothek Mathematik, 2003.
date_created: 2018-12-11T12:04:34Z
date_published: 2003-03-31T00:00:00Z
date_updated: 2021-01-12T07:45:05Z
day: '31'
extern: 1
intvolume: ' 356'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/~chl/papers/lampert-phd2003.pdf
month: '03'
page: 1 - 165
publication: Bonner Mathematische Schriften
publication_status: published
publisher: Universität Bonn, Fachbibliothek Mathematik
publist_id: '2704'
quality_controlled: 0
status: public
title: 'The Neumann operator in strictly pseudoconvex domains with weighted Bergman
metric '
type: dissertation
volume: 356
year: '2003'
...
---
_id: '4414'
abstract:
- lang: eng
text: "This dissertation investigates game-theoretic approaches to the algorithmic
analysis of concurrent, reactive systems. A concurrent system comprises a number
of components working concurrently; a reactive system maintains an ongoing interaction
with its environment. Traditional approaches to the formal analysis of concurrent
reactive systems usually view the system as an unstructured state-transition graphs;
instead, we view them as collections of interacting components, where each one
is an open system which accepts inputs from the other components. The interactions
among the components are naturally modeled as games.\r\n\r\nAdopting this game-theoretic
view, we study three related problems pertaining to the verification and synthesis
of systems. Firstly, we propose two novel game-theoretic techniques for the model-checking
of concurrent reactive systems, and improve the performance of model-checking.
The first technique discovers an error as soon as it cannot be prevented, which
can be long before it actually occurs. This technique is based on the key observation
that "unpreventability" is a local property to a module: an error is
unpreventable in a module state if no environment can prevent it. The second technique
attempts to decompose a model-checking proof into smaller proof obligations by
constructing abstract modules automatically, using reachability and "unpreventability"
information about the concrete modules. Three increasingly powerful proof decomposition
rules are proposed and we show that in practice, the resulting abstract modules
are often significantly smaller than the concrete modules and can drastically
reduce the space and time requirements for verification. Both techniques fall
into the category of compositional reasoning.\r\n\r\nSecondly, we investigate
the composition and control of synchronous systems. An essential property of synchronous
systems for compositional reasoning is non-blocking. In the composition of synchronous
systems, however, due to circular causal dependency of input and output signals,
non-blocking is not always guaranteed. Blocking compositions of systems can be
ruled out semantically, by insisting on the existence of certain fixed points,
or syntactically, by equipping systems with types, which make the dependencies
between input and output signals transparent. We characterize various typing mechanisms
in game-theoretic terms, and study their effects on the controller synthesis problem.
We show that our typing systems are general enough to capture interesting real-life
synchronous systems such as all delay-insensitive digital circuits. We then study
their corresponding single-step control problems --a restricted form of controller
synthesis problem whose solutions can be iterated in appropriate manners to solve
all LTL controller synthesis problems. We also consider versions of the controller
synthesis problem in which the type of the controller is given. We show that the
solution of these fixed-type control problems requires the evaluation of partially
ordered (Henkin) quantifiers on boolean formulas, and is therefore harder (nondeterministic
exponential time) than more traditional control questions.\r\n\r\nThirdly, we
study the synthesis of a class of open systems, namely, uninitialized state machines.
The sequential synthesis problem, which is closely related to Church's solvability
problem, asks, given a specification in the form of a binary relation between
input and output streams, for the construction of a finite-state stream transducer
that converts inputs to appropriate outputs. For efficiency reasons, practical
sequential hardware is often designed to operate without prior initialization.
Such hardware designs can be modeled by uninitialized state machines, which are
required to satisfy their specification if started from any state. We solve the
sequential synthesis problem for uninitialized systems, that is, we construct
uninitialized finite-state stream transducers. We consider specifications given
by LTL formulas, deterministic, nondeterministic, universal, and alternating Buechi
automata. We solve this uninitialized synthesis problem by reducing it to the
well-understood initialized synthesis problem. While our solution is straightforward,
it leads, for some specification formalisms, to upper bounds that are exponentially
worse than the complexity of the corresponding initialized problems. However,
we prove lower bounds to show that our simple solutions are optimal for all considered
specification formalisms. The lower bound proofs require nontrivial generic reductions."
article_processing_charge: No
author:
- first_name: Freddy
full_name: Mang, Freddy
last_name: Mang
citation:
ama: Mang F. Games in open systems verification and synthesis. 2002:1-116.
apa: Mang, F. (2002). *Games in open systems verification and synthesis*. University
of California, Berkeley.
chicago: Mang, Freddy. “Games in Open Systems Verification and Synthesis.” University
of California, Berkeley, 2002.
ieee: F. Mang, “Games in open systems verification and synthesis,” University of
California, Berkeley, 2002.
ista: Mang F. 2002. Games in open systems verification and synthesis. University
of California, Berkeley.
mla: Mang, Freddy. *Games in Open Systems Verification and Synthesis*. University
of California, Berkeley, 2002, pp. 1–116.
short: F. Mang, Games in Open Systems Verification and Synthesis, University of
California, Berkeley, 2002.
date_created: 2018-12-11T12:08:44Z
date_published: 2002-05-01T00:00:00Z
date_updated: 2021-01-12T07:56:48Z
day: '01'
extern: '1'
language:
- iso: eng
month: '05'
oa_version: None
page: 1 - 116
publication_status: published
publisher: University of California, Berkeley
publist_id: '315'
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: Games in open systems verification and synthesis
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2002'
...
---
_id: '4411'
abstract:
- lang: eng
text: "Model checking algorithms for the verification of reactive systems proceed
by a systematic and exhaustive exploration of the system state space. They do
not scale to large designs because of the state explosion problem --the number
of states grows exponentially with the number of components in the design. Consequently,
the model checking problem is PSPACE-hard in the size of the design description.
This dissertation proposes three novel techniques to combat the state explosion
problem.\r\n\r\nOne of the most important advances in model checking in recent
years has been the discovery of symbolic methods, which use a calculus of expressions,
such as binary decision diagrams, to represent the state sets encountered during
state space exploration. Symbolic model checking has proved to be effective for
verifying hardware designs. Traditionally, symbolic checking of temporal logic
specifications is performed by backward fixpoint reasoning with the operator Pre.
Backward reasoning can be wasteful since unreachable states are explored. We suggest
the use of forward fixpoint reasoning based on the operator Post. We show how
all linear temporal logic specifications can be model checked symbolically by
forward reasoning. In contrast to backward reasoning, forward reasoning performs
computations only on the reachable states.\r\n\r\nHeuristics that improve algorithms
for application domains, such as symbolic methods for hardware designs, are useful
but not enough to make model checking feasible on industrial designs. Currently,
exhaustive state exploration is possible only on designs with about 50-100 boolean
state variables. Assume-guarantee verification attempts to combat the state explosion
problem by using the principle of "divide and conquer," where the components
of the implementation are analyzed one at a time. Typically, an implementation
component refines its specification only when its inputs are suitably constrained
by other components in the implementation. The assume-guarantee principle states
that instead of constraining the inputs by implementation components, it is sound
to constrain them by the corresponding specification components, which can be
significantly smaller. We extend the assume-guarantee proof rule to deal with
the case where the specification operates at a coarser time scale than the implementation.
Using our model checker Mocha, which implements this methodology, we verify VGI,
a parallel DSP processor chip with 64 compute processors each containing approximately
800 state variables and 30K gates.\r\n\r\nOur third contribution is a systematic
model checking methodology for verifying the abstract shared-memory interface
of sequential consistency on multiprocessor systems with three parameters --number
of processors, number of memory locations, and number of data values. Sequential
consistency requires that some interleaving of the local temporal orders of read/write
events at different processors be a trace of serial memory. Therefore, it suffices
to construct a non-interfering serializer that watches and reorders read/write
events so that a trace of serial memory is obtained. While in general such a serializer
must be unbounded even for fixed values of the parameters --checking sequential
consistency is undecidable!-- we show that the paradigmatic class of snoopy cache
coherence protocols has finite-state serializers. In order to reduce the arbitrary-parameter
problem to the fixed-parameter problem, we develop a novel framework for induction
over the number of processors and use the notion of a serializer to reduce the
problem of verifying sequential consistency to that of checking language inclusion
between finite state machines."
article_processing_charge: No
author:
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
citation:
ama: Qadeer S. Algorithms and Methodology for Scalable Model Checking. 1999:1-150.
apa: Qadeer, S. (1999). *Algorithms and Methodology for Scalable Model Checking*.
University of California, Berkeley.
chicago: Qadeer, Shaz. “Algorithms and Methodology for Scalable Model Checking.”
University of California, Berkeley, 1999.
ieee: S. Qadeer, “Algorithms and Methodology for Scalable Model Checking,” University
of California, Berkeley, 1999.
ista: Qadeer S. 1999. Algorithms and Methodology for Scalable Model Checking. University
of California, Berkeley.
mla: Qadeer, Shaz. *Algorithms and Methodology for Scalable Model Checking*.
University of California, Berkeley, 1999, pp. 1–150.
short: S. Qadeer, Algorithms and Methodology for Scalable Model Checking, University
of California, Berkeley, 1999.
date_created: 2018-12-11T12:08:43Z
date_published: 1999-10-01T00:00:00Z
date_updated: 2021-01-12T07:56:47Z
day: '01'
extern: '1'
language:
- iso: eng
main_file_link:
- url: http://mtc.epfl.ch/~tah/Students/qadeer.pdf
month: '10'
oa_version: None
page: 1 - 150
publication_status: published
publisher: University of California, Berkeley
publist_id: '321'
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Robert
full_name: Bryton, Robert
last_name: Bryton
- first_name: John
full_name: Steel, John
last_name: Steel
title: Algorithms and Methodology for Scalable Model Checking
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '1999'
...
---
_id: '4419'
article_processing_charge: No
author:
- first_name: Peter
full_name: Kopke, Peter
last_name: Kopke
citation:
ama: Kopke P. The Theory of Rectangular Hybrid Automata. 1996.
apa: Kopke, P. (1996). *The Theory of Rectangular Hybrid Automata*. Cornell
University.
chicago: Kopke, Peter. “The Theory of Rectangular Hybrid Automata.” Cornell University,
1996.
ieee: P. Kopke, “The Theory of Rectangular Hybrid Automata,” Cornell University,
1996.
ista: Kopke P. 1996. The Theory of Rectangular Hybrid Automata. Cornell University.
mla: Kopke, Peter. *The Theory of Rectangular Hybrid Automata*. Cornell University,
1996.
short: P. Kopke, The Theory of Rectangular Hybrid Automata, Cornell University,
1996.
date_created: 2018-12-11T12:08:45Z
date_published: 1996-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:50Z
day: '01'
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
publication_status: published
publisher: Cornell University
publist_id: '312'
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: The Theory of Rectangular Hybrid Automata
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '1996'
...