|
|
|
|
Improved State Space Reductions for LTL Model Checking of C and C++ Programs |
|
|
1 | (15) |
|
|
|
|
|
|
|
Regular Model Checking Using Solver Technologies and Automata Learning |
|
|
16 | (16) |
|
|
|
|
|
Improved on-the-Fly Livelock Detection: Combining Partial Order Reduction and Parallelism for DFSFIFO |
|
|
32 | (16) |
|
|
|
|
|
Session 2 Applications of Formal Methods |
|
|
|
Evaluating Human-Human Communication Protocols with Miscommunication Generation and Model Checking |
|
|
48 | (15) |
|
|
|
|
|
Using Model-Checking to Reveal a Vulnerability of Tamper-Evident Pairing |
|
|
63 | (15) |
|
|
|
|
|
|
|
|
|
|
|
SMT-Based Analysis of Biological Computation |
|
|
78 | (15) |
|
|
|
Christoph M. Wintersteiger |
|
|
|
|
|
|
Session 3 Complex Systems |
|
|
|
Freshness and Reactivity Analysis in Globally Asynchronous Locally Time-Triggered Systems |
|
|
93 | (15) |
|
|
|
|
|
|
|
|
|
Enclosing Temporal Evolution of Dynamical Systems Using Numerical Methods |
|
|
108 | (16) |
|
|
|
|
|
|
|
Inferring Automata with State-Local Alphabet Abstractions |
|
|
124 | (15) |
|
|
|
|
|
|
|
Session 4 Static Analysis |
|
|
|
Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers |
|
|
139 | (16) |
|
|
|
|
|
|
|
Numerical Abstract Domain Using Support Functions |
|
|
155 | (15) |
|
|
|
|
|
Widening as Abstract Domain |
|
|
170 | (15) |
|
|
|
|
|
|
|
LiquidPi: Inferrable Dependent Session Types |
|
|
185 | (13) |
|
|
|
|
|
Session 5 Symbolic Execution |
|
|
|
Automated Verification of Chapel Programs Using Model Checking and Symbolic Execution |
|
|
198 | (15) |
|
|
|
|
|
|
|
Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-Bounding |
|
|
213 | (16) |
|
|
|
|
|
|
|
|
|
Bounded Lazy Initialization |
|
|
229 | (15) |
|
|
|
|
|
|
|
|
|
Session 6 Requirements and Specifications |
|
|
|
From UML to Process Algebra and Back: An Automated Approach to Model-Checking Software Design Artifacts of Concurrent Systems |
|
|
244 | (17) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Automatically Detecting Inconsistencies in Program Specifications |
|
|
261 | (15) |
|
|
|
|
|
BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software |
|
|
276 | (15) |
|
|
|
|
|
|
|
Towards Complete Specifications with an Error Calculus |
|
|
291 | (16) |
|
|
|
|
|
|
|
|
|
Session 7 Probabilistic and Statistical Analysis |
|
|
|
A Probabilistic Quantitative Analysis of Probabilistic---Write/Copy-Select |
|
|
307 | (15) |
|
|
|
|
|
|
|
|
|
|
|
|
|
Statistical Model Checking of Wireless Mesh Routing Protocols |
|
|
322 | (15) |
|
|
|
|
|
On-the-Fly Confluence Detection for Statistical Model Checking |
|
|
337 | (15) |
|
|
|
|
|
Optimizing Control Strategy Using Statistical Model Checking |
|
|
352 | (16) |
|
|
|
|
|
|
|
|
|
|
|
Session 8 Theorem Proving |
|
|
|
Formal Stability Analysis of Optical Resonators |
|
|
368 | (15) |
|
|
|
|
|
|
|
Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations |
|
|
383 | (15) |
|
|
|
|
|
Verifying a Privacy CA Remote Attestation Protocol |
|
|
398 | (15) |
|
|
|
|
|
Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory |
|
|
413 | (15) |
|
|
|
|
|
|
|
|
|
|
Formal Verification of a Parameterized Data Aggregation Protocol |
|
|
428 | (7) |
|
|
|
|
|
OnTrack: An Open Tooling Environment for Railway Verification |
|
|
435 | (6) |
|
|
|
|
|
|
|
|
|
|
|
Verification of Numerical Programs: From Real Numbers to Floating Point Numbers |
|
|
441 | (6) |
|
|
|
|
|
|
|
|
|
Extracting Hybrid Automata from Control Code |
|
|
447 | (6) |
|
|
|
|
|
PyNuSMV: NuSMV as a Python Library |
|
|
453 | (6) |
|
|
|
|
|
jUnitRV---Adding Runtime Verification to jUnit |
|
|
459 | (6) |
|
|
|
|
|
|
|
Using Language Engineering to Lift Languages and Analyses at the Domain Level |
|
|
465 | (7) |
|
|
|
|
|
|
|
|
|
On Designing an ACL2-Based C Integer Type Safety Checking Tool |
|
|
472 | (6) |
|
|
|
|
|
Hierarchical Safety Cases |
|
|
478 | (7) |
|
|
|
|
|
|
| Author Index |
|
485 | |
Lisainfo e-raamatute kohta