Springer Science and Business Media LLC
Công bố khoa học tiêu biểu
* Dữ liệu chỉ mang tính chất tham khảo
Sắp xếp:
Introducing robust reachability
Springer Science and Business Media LLC - - Trang 1-29 - 2022
We introduce a new property called robust reachability which refines the standard notion of reachability in order to take replicability into account. A bug is robustly reachable if a controlled input can make it so the bug is reached whatever the value of uncontrolled input. Robust reachability is better suited than standard reachability in many realistic situations related to security (e.g., crit......
Achieving distributed control through model checking
Springer Science and Business Media LLC - Tập 40 - Trang 263-281 - 2012
We apply model checking of knowledge properties to the design of distributed controllers that enforce global constraints on concurrent systems. The problem of synthesizing a distributed controller is undecidable in the general case. We thus look at a variant of the synthesis problem that allows adding temporary synchronizations between processes. We calculate when processes can decide autonomously......
Refutation-based synthesis in SMT
Springer Science and Business Media LLC - Tập 55 - Trang 73-102 - 2017
We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided techniques for quantifier instantiation that we use to make finding such proofs practically feasible. A particularly important class of specifi......
A Formal Verification Environment for Railway Signaling System Design
Springer Science and Business Media LLC - Tập 12 - Trang 139-161 - 1998
A fundamental problem in the design and development of embedded control systems is the verification of safety requirements. Formal methods, offering a mathematical way to specify and analyze the behavior of a system, together with the related support tools can successfully be applied in the formal proof that a system is safe. However, the complexity of real systems is such that automated tools oft......
Probabilistic verification of Boolean functions
Springer Science and Business Media LLC - Tập 1 - Trang 61-115 - 1992
We present a novel method for verifying the equivalence of two Boolean functions. Each function is hashed to an integer code by assigning random integer values to the input variables and evaluating an integer-valued transformation of the original function. The hash codes for two equivalent functions are always equal. Thus the equivalence of two functions can be verified with a very low probability......
Exploring structural symmetry automatically in symbolic trajectory evaluation
Springer Science and Business Media LLC - Tập 39 Số 2 - Trang 117-143 - 2011
Enhancing active model learning with equivalence checking using simulation relationsAbstract We present a new active model-learning approach to generating abstractions of a system from its execution traces. Given a system and a set of observables to collect execution traces, the abstraction produced by the algorithm is guaranteed to admit all system traces over the set of observables. To achieve this, the approach uses a pluggable model-learning co... ...
Springer Science and Business Media LLC - - 2022
Functional synthesis via input–output separation
Springer Science and Business Media LLC - Tập 60 - Trang 228-258 - 2023
Boolean functional synthesis is the process of constructing a Boolean function from a Boolean specification that relates input and output variables. Despite recent developments in synthesis algorithms, Boolean functional synthesis remains a challenging problem even when state-of-the-art techniques are used for decomposing the specification. In this work, we present a new decomposition approach tha......
Tổng số: 485
- 1
- 2
- 3
- 4
- 5
- 6
- 10