Abstract is missing.
- Formal Proofs of Code Generation and Verification ToolsXavier Leroy. 1-4 [doi]
- Lightweight Program Construction and Verification Tools in Isabelle/HOLAlasdair Armstrong, Victor B. F. Gomes, Georg Struth. 5-19 [doi]
- Completeness of Separation Logic with Inductive Definitions for Program VerificationMakoto Tatsuta, Wei-Ngan Chin. 20-34 [doi]
- A Thread-Safe Library for Binary Decision DiagramsAlberto Lovato, Damiano Macedonio, Fausto Spoto. 35-49 [doi]
- Effect-Polymorphic Behaviour Inference for Deadlock CheckingKa-I Pun, Martin Steffen, Volker Stolz. 50-64 [doi]
- Synthesizing Parameterized Unit Tests to Detect Object Invariant ViolationsMaria Christakis, Peter Müller, Valentin Wüstholz. 65-80 [doi]
- Formalizing DSL Semantics for Reasoning and Conformance TestingSarmen Keshishzadeh, Arjan J. Mooij. 81-95 [doi]
- Test Suite Completeness and Partial ModelsAdilson Luiz Bonifácio, Arnaldo Vieira Moura. 96-110 [doi]
- Automated Error-Detection and Repair for Compositional Software SpecificationsDalal Alrajeh, Robert Craven. 111-127 [doi]
- A General Framework for Architecture ComposabilityPaul C. Attie, Eduard Baranov, Simon Bliudze, Mohamad Jaber, Joseph Sifakis. 128-143 [doi]
- Trace Checking of Metric Temporal Logic with Aggregating Modalities Using MapReduceDomenico Bianculli, Carlo Ghezzi, Srdan Krstic. 144-158 [doi]
- Increasing Consistency in Multi-site Data Stores: Megastore-CGC and Its Formal AnalysisJon Grov, Peter Csaba Ölveczky. 159-174 [doi]
- Evaluating the Effect of Faults in SystemC TLM Models Using UPPAALReza Hajisheykhi, Ali Ebnenasir, Sandeep S. Kulkarni. 175-189 [doi]
- Formal Verification of Discrete-Time MATLAB/Simulink Models Using BoogieRobert Reicherdt, Sabine Glesner. 190-204 [doi]
- A Formal Model for Constraint-Based Deployment Calculation and Analysis for Fault-Tolerant SystemsKlaus Becker, Bernhard Schätz, Michael Armbruster, Christian Buckl. 205-219 [doi]
- Optimising the ProB Model Checker for B Using Partial Order ReductionIvaylo Dobrikov, Michael Leuschel. 220-234 [doi]
- Rapid Prototyping of a Semantically Well Founded Circus Model CheckerAlexandre Mota, Adalberto Farias, André Didier, Jim Woodcock. 235-249 [doi]
- Learning Extended Finite State MachinesSofia Cassel, Falk Howar, Bengt Jonsson, Bernhard Steffen. 250-264 [doi]
- Translating Event-B Machines to Database ApplicationsQi Wang, Tim Wahls. 265-270 [doi]
- IKOS: A Framework for Static Analysis Based on Abstract InterpretationGuillaume Brat, Jorge A. Navas, Nija Shi, Arnaud Venet. 271-277 [doi]
- A Toolset for Support of Teaching Formal Software DevelopmentStefan Korecko, Ján Sorád, Zuzana Dudláková, Branislav Sobota. 278-283 [doi]
- Execution and Verification of UML State Machines with ErlangRicardo J. Rodríguez, Lars-Åke Fredlund, Ángel Herranz-Nieva, Julio Mariño. 284-289 [doi]
- A Tool for Verifying Dynamic Properties in BFama Diagne, Amel Mammar, Marc Frappier. 290-295 [doi]
- WeVerca: Web Applications Verification for PHPDavid Hauzar, Jan Kofron. 296-301 [doi]
- More Flexible Object Invariants with Less Specification OverheadStefan Huster, Patrick Heckeler, Hanno Eichelberger, Jürgen Ruf, Sebastian Burg, Thomas Kropf, Wolfgang Rosenstiel. 302-316 [doi]
- Verified Functional Iterators Using the FoCaLiZe EnvironmentCatherine Dubois, Renaud Rioboo. 317-331 [doi]
- Tool Support for Teaching Hoare LogicTadeusz Sznuk, Aleksy Schubert. 332-346 [doi]
- A Two-Phase Static Analysis for Reliable AdaptationPierpaolo Degano, Gian Luigi Ferrari, Letterio Galletta. 347-362 [doi]
- Formal Modelling and Verification of Cooperative Ant Behaviour in Event-BLinas Laibinis, Elena Troubitsyna, zeineb graja, Frédéric Migeon, Ahmed Hadj Kacem. 363-377 [doi]
- A Formal Privacy Policy Framework for Social NetworksRaúl Pardo, Gerardo Schneider. 378-392 [doi]