Zobrazeno 1 - 10
of 236
pro vyhledávání: '"Zohar Manna"'
Autor:
Aaron R. Bradley, Zohar Manna
Publikováno v:
Formal Aspects of Computing. 20:379-405
A fundamental method of analyzing a system such as a program or a circuit is invariance analysis, in which one proves that an assertion holds on all reachable states. Typically, the proof is performed via induction; however, an assertion, while invar
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4c59d5362825cfa0c411c83fac93de40
https://doi.org/10.1007/s00165-008-0080-9
https://doi.org/10.1007/s00165-008-0080-9
Publikováno v:
Formal Aspects of Computing. 20:507-560
Alternating systems are models of computer programs whose behavior is governed by the actions of multiple agents with, potentially, different goals. Examples include control systems, resource schedulers, security protocols, auctions and election mech
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::71ccf7c61b565903e394627c1607d90c
https://doi.org/10.1007/s00165-008-0075-6
https://doi.org/10.1007/s00165-008-0075-6
Publikováno v:
Formal Methods in System Design. 32:25-55
We present a new method for generating algebraic invariants of hybrid systems. The method reduces the invariant generation problem to a constraint solving problem using techniques from the theory of ideals over polynomial rings. Starting with a templ
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d7722d9e8804f45074fea5b17da6aedc
https://doi.org/10.1007/s10703-007-0046-1
https://doi.org/10.1007/s10703-007-0046-1
Publikováno v:
POPL
We present a new technique for the generation of non-linear (algebraic) invariants of a program. Our technique uses the theory of ideals over polynomial rings to reduce the non-linear invariant generation problem to a numerical constraint solving pro
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4043e62b3bba5e942dff94dfa727f423
https://doi.org/10.1145/982962.964028
https://doi.org/10.1145/982962.964028
Publikováno v:
Theoretical Computer Science. 253(1):27-60
We present a modular framework for proving temporal properties of real-time systems, based on clocked transition systems and linear-time temporal logic. We show how deductive verification rules, verification diagrams, and automatic invariant generati
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1f56192643b4d68138c35db97d8e2bbf
Publikováno v:
Acta Informatica. 36:837-912
This paper presents a new computational model for real-time systems, called the clocked transition system (CTS) model. The CTS model is a development of our previous timed transition model, where some of the changes are inspired by the model of timed
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::689a45e96969ffdac3055ef1b857c600
https://doi.org/10.1007/s002360050177
https://doi.org/10.1007/s002360050177
Autor:
Zohar Manna, Michael Colón, Tomás E. Uribe, Nikolaj Bjørner, Henny B. Sipma, Anca Browne, Bernd Finkbeiner
Publikováno v:
Formal Methods in System Design. 16:227-270
We review a number of formal verification techniques supported by STeP, the Stanford Temporal Prover, describing how the tool can be used to verify properties of several versions of the Bakery Mutual exclusion algorithm for mutual exclusion. We verif
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6602a7bd67f1de3f7f020ea5becbbbbe
https://doi.org/10.1023/a:1008700623084
https://doi.org/10.1023/a:1008700623084
Publikováno v:
Formal Methods in System Design. 15:49-74
We present an extension of classical tableau-based model checking procedures to the case of infinite-state systems, using deductive methods in an incremental construction of the behavior graph. Logical formulas are used to represent infinite sets of
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::43824f10427b1f21f72a5dc6398c1d8f
https://doi.org/10.1023/a:1008791913551
https://doi.org/10.1023/a:1008791913551
Autor:
Zohar Manna, Amir Pnueli
Reactive systems are computing systems which are interactive, such as real-time systems, operating systems, concurrent systems, control systems, etc. They are among the most difficult computing systems to program. Temporal logic is a formal tool/lang
Autor:
Zohar Manna, Amir Pnueli
This book is about the verification of reactive systems. A reactive system is a system that maintains an ongoing interaction with its environment, as opposed to computing some final value on termination. The family of reactive systems includes many c