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:
An Implementation of Constructive Synchronous Programs in POLIS
Springer Science and Business Media LLC - - 2000
Design tools for embedded reactive systems commonly use a model of computation that employs both synchronous and asynchronous communication styles. We form a junction between these two with an implementation of synchronous languages and circuits (Esterel) on asynchronous networks (POLIS). We implement fact propagation, the key concept of synchronous constructive semantics, on an asynchronous non-d......
Cut-off theorems for the PV-model
Springer Science and Business Media LLC - Tập 59 - Trang 21-43 - 2022
For a PV thread T which accesses a set
$$\mathcal {R}$$
of resources, each with a maximal capacity
$$\kappa :\mathcal {R}\rightarrow {\mathbb {N}}$$
, the PV-program
......
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......
An Efficient Algorithm for Minimizing Real-Time Transition Systems
Springer Science and Business Media LLC - Tập 11 - Trang 113-136 - 1997
We address the problem of performing simultaneously reachability analysis and minimization of real-time transition systems represented by timed automata, i.e., automata extended with a finite set of clock variables. The transitions of the automaton may depend on the values of the clocks and may reset some of the clocks. An efficient algorithm is presented for minimizing a system with respect to a ......
2009 CAV award announcement
Springer Science and Business Media LLC - Tập 36 - Trang 195-197 - 2010
The 2009 CAV (Computer-Aided Verification) award was presented to seven individuals who made major advances in creating high-performance Boolean satisfiability solvers. This annual award recognizes a specific fundamental contribution or series of outstanding contributions to the CAV field.
Antichains and compositional algorithms for LTL synthesis
Springer Science and Business Media LLC - Tập 39 - Trang 261-296 - 2011
In this paper, we present new monolithic and compositional algorithms to solve the LTL realizability problem. Those new algorithms are based on a reduction of the LTL realizability problem to a game whose winning condition is defined by a universal automaton on infinite words with a k-co-Büchi acceptance condition. This acceptance condition asks that runs visit at most k accepting states, so it im......
Debug-localize-repair: a symbiotic construction for heap manipulations
Springer Science and Business Media LLC - Tập 58 - Trang 399-439 - 2022
We present Wolverine2, an integrated Debug-Localize-Repair environment for heap manipulating programs. Wolverine2 provides an interactive debugging environment: while concretely executing a program via on an interactive shell supporting common debugging facilities, Wolverine2 displays the abstract program states (as box-and-arrow diagrams) as a visual aid to the programmer, packages a novel, proof......
Tổng số: 485
- 1
- 2
- 3
- 4
- 5
- 6
- 10