default search action
24th SPIN(@ISSTA) 2017: Santa Barbara, CA, USA
- Hakan Erdogmus, Klaus Havelund:
Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, Santa Barbara, CA, USA, July 10-14, 2017. ACM 2017, ISBN 978-1-4503-5077-8
Invited Papers
- Gerard J. Holzmann:
Cobra: fast structural code checking (keynote). 1-8 - Byron Cook:
Automated formal reasoning about amazon web services (keynote). 9 - Domagoj Babic:
SunDew: systematic automated security testing (keynote). 10
Reports
- Marc Jasper, Maximilian Fecke, Bernhard Steffen, Markus Schordan, Jeroen Meijer, Jaco van de Pol, Falk Howar, Stephen F. Siegel:
The RERS 2017 challenge and workshop (invited paper). 11-20
Symbolic Verification
- Wytse Oortwijn, Tom van Dijk
, Jaco van de Pol:
Distributed binary decision diagrams for symbolic reachability. 21-30
Model Checking I
- Heila Botha, Oksana Tkachuk, Brink van der Merwe, Willem Visser:
Addressing challenges in obtaining high coverage when model checking Android applications. 31-40 - Pouria Mellati, Ehsan Khamespanah, Ramtin Khosravi:
LeeTL: LTL with quantifications over model objects. 41-49 - Vincent Bloemen, Alexandre Duret-Lutz
Explicit state model checking with generalized Büchi and Rabin automata. 50-59
Code Verification
- Daniel Ratiu, Andreas Ulrich:
Increasing usability of spin-based C code verification using a harness definition language: leveraging model-driven code checking to practitioners. 60-69
Runtime Enforcement
- Matthieu Renard, Antoine Rollet, Yliès Falcone:
Runtime enforcement using Büchi games. 70-79 - Srinivas Pinisetty
Runtime enforcement of reactive systems using synchronous enforcers. 80-89
Model Checking - Short Papers
- Lucas G. Wagner, David A. Greve, Andrew Gacek:
SIMPAL: a compositional reasoning framework for imperative programs. 90-93 - Marco A. Feliú
Verification-driven development of ICAROUS based on automatic reachability analysis: a preliminary case study. 94-97 - Marcello M. Bersani, Francesco Marconi, Matteo Rossi, Madalina Erascu
Formal verification of data-intensive applications through model checking modulo theories. 98-101
Program Synthesis
- Guangyuan Li, Peter Gjøl Jensen
Practical controller synthesis for MTL0, ∞. 102-111 - John Fearnley, Sanjay Jain, Sven Schewe
An ordered approach to solving parity games in quasi polynomial time and quasi linear space. 112-121 - Idress Husien, Nicolas Berthier
A hot method for synthesising cool controllers. 122-131
Model Checking II
- Thomas Geffroy, Jérôme Leroux, Grégoire Sutre:
Backward coverability with pruning for lossy channel systems. 132-141 - Paul Fiterau-Brostean, Toon Lenaerts, Erik Poll, Joeri de Ruiter
Model learning and model checking of SSH implementations. 142-151 - Huu-Vu Nguyen, Tayssir Touili:
CARET model checking for malware detection. 152-161
Program Sketching
- Jinru Hua, Sarfraz Khurshid:
EdSketch: execution-driven sketching for Java. 162-171
Testing
- Michalis Kokologiannakis
Stateless model checking of the Linux kernel's hierarchical read-copy-update (tree RCU). 172-181 - Nima Dini, Cagdas Yelen, Sarfraz Khurshid:
Optimizing parallel Korat using invalid ranges. 182-191
Testing - Short Papers
- Laura Panizo
Guided test case generation for mobile apps in the TRIANGLE project: work in progress. 192-195 - Blake Loring, Duncan Mitchell, Johannes Kinder:
ExpoSE: practical symbolic execution of standalone JavaScript. 196-199
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-01-13 01:12 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: