Abstract is missing.
- Abstractions, Semantic Models and Analysis Tools for Concurrent Systems: Progress and Open Problems - (Extended Abstract)Gul Agha. 3-8 [doi]
- Satisfiability Checking: Theory and ApplicationsErika Ábrahám, Gereon Kremer. 9-23 [doi]
- Automatic Derivation of Platform Noninterference PropertiesOliver Schwarz, Mads Dam. 27-44 [doi]
- Linearizability and CausalitySimon Doherty, John Derrick. 45-60 [doi]
- Refinement-Based Verification of Communicating Unstructured CodeNils Jähnig, Thomas Göthel, Sabine Glesner. 61-75 [doi]
- Guided Dynamic Symbolic Execution Using Subgraph Control-Flow InformationJosselin Feist, Laurent Mounier, Marie-Laure Potet. 76-81 [doi]
- Correlating Structured Inputs and Outputs in Functional SpecificationsOana Fabiana Andreescu, Thomas Jensen, Stéphane Lescuyer. 85-103 [doi]
- Combining Predicate Abstraction with Fixpoint ApproximationsTuba Yavuz. 104-120 [doi]
- Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements AnalysisJaroslav Bendík, Nikola Benes, Jiri Barnat, Ivana Cerná. 121-136 [doi]
- Combining Abstract Interpretation with Symbolic Execution for a Static Value Range Analysis of Block DiagramsChristian Dernehl, Norman Hansen, Stefan Kowalewski. 137-152 [doi]
- Program Generation Using Simulated Annealing and Model CheckingIdress Husien, Sven Schewe. 155-171 [doi]
- LTL Parameter Synthesis of Parametric Timed AutomataPeter Bezdek, Nikola Benes, Jiri Barnat, Ivana Cerná. 172-187 [doi]
- Model Checking Simulation Rules for LinearizabilityGraeme Smith. 188-203 [doi]
- LTL Model Checking under Fairness in ProBIvaylo Dobrikov, Michael Leuschel, Daniel Plagge. 204-211 [doi]
- Counterexamples from Proof Failures in SPARKDavid Hauzar, Claude Marché, Yannick Moy. 215-233 [doi]
- Proving Termination of Programs with Bitvector Arithmetic by Symbolic ExecutionJera Hensel, Jürgen Giesl, Florian Frohn, Thomas Ströder. 234-252 [doi]
- SMT-Based Automatic Proof of ASM Model RefinementPaolo Arcaini, Angelo Gargantini, Elvinia Riccobene. 253-269 [doi]
- Coq Implementation of OO Verification Framework VeriJKe Zhang, Zongyan Qiu. 270-276 [doi]
- Towards a Proof Framework for Information Systems with Weak ConsistencyPeter Zeller, Arnd Poetzsch-Heffter. 277-283 [doi]
- A Cognitive Framework Based on Rewriting Logic for the Analysis of Interactive SystemsAntonio Cerone. 287-303 [doi]
- Incentive Stackelberg Mean-Payoff GamesAnshul Gupta, Sven Schewe, Ashutosh Trivedi, Maram Sai Krishna Deepak, Bharath Kumar Padarthi. 304-320 [doi]
- Stability-Based Adaptation of Asynchronously Communicating SoftwareCarlos Canal, Gwen Salaün. 321-336 [doi]
- Compliance Checking in the Open Payments EcosystemShaun Azzopardi, Christian Colombo, Gordon J. Pace, Brian Vella. 337-343 [doi]
- CoCoSpec: A Mode-Aware Contract Language for Reactive SystemsAdrien Champion, Arie Gurfinkel, Temesghen Kahsai, Cesare Tinelli. 347-366 [doi]
- Modularizing Crosscutting Concerns in Component-Based SystemsAntoine El-Hokayem, Yliès Falcone, Mohamad Jaber. 367-385 [doi]
- Tightening a Contract RefinementAlessandro Cimatti, Ramiro Demasi, Stefano Tonetta. 386-402 [doi]
- BMotionWeb: A Tool for Rapid Creation of Formal PrototypesLukas Ladenberger, Michael Leuschel. 403-417 [doi]