Abstract is missing.
- Validity Checking of Putback Transformations in Bidirectional ProgrammingZhenjiang Hu, Hugo Pacheco, Sebastian Fischer. 1-15 [doi]
- Proof Engineering Considered EssentialGerwin Klein. 16-21 [doi]
- Engineering UToPiA - Formal Semantics for CMLJim Woodcock. 22-41 [doi]
- 40 Years of Formal Methods - Some Obstacles and Some Possibilities?Dines Bjørner, Klaus Havelund. 42-61 [doi]
- A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP ProcessesPedro R. G. Antonino, Augusto Sampaio, Jim Woodcock. 62-77 [doi]
- Algebraic Principles for Rely-Guarantee Style Concurrency Verification ToolsAlasdair Armstrong, Victor B. F. Gomes, Georg Struth. 78-93 [doi]
- Definition, Semantics, and Analysis of Multirate Synchronous AADLKyungmin Bae, Peter Csaba Ölveczky, José Meseguer. 94-109 [doi]
- TrustFound: Towards a Formal Foundation for Model Checking Trusted Computing PlatformsGuangdong Bai, Jianan Hao, Jianliang Wu, Yang Liu, Zhenkai Liang, Andrew Martin. 110-126 [doi]
- The VerCors Tool for Verification of Concurrent ProgramsStefan Blom, Marieke Huisman. 127-131 [doi]
- Knowledge-Based Automated Repair of Authentication ProtocolsBorzoo Bonakdarpour, Reza Hajisheykhi, Sandeep S. Kulkarni. 132-147 [doi]
- A Simplified Z Semantics for Presentation Interaction ModelsJudy Bowen, Steve Reeves. 148-162 [doi]
- Log Analysis for Data Protection AccountabilityDenis Butin, Daniel Le Métayer. 163-178 [doi]
- Automatic Compositional Synthesis of Distributed SystemsWerner Damm, Bernd Finkbeiner. 179-193 [doi]
- Automated Real Proving in PVS via MetiTarskiWilliam Denman, César Muñoz. 194-199 [doi]
- Quiescent Consistency: Defining and Verifying Relaxed LinearizabilityJohn Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, Heike Wehrheim. 200-214 [doi]
- Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing ProtocolParasara Sridhar Duggirala, Le Wang, Sayan Mitra, Mahesh Viswanathan, César Muñoz. 215-229 [doi]
- Contracts in PracticeH.-Christian Estler, Carlo A. Furia, Martin Nordio, Marco Piccioni, Bertrand Meyer. 230-246 [doi]
- When Equivalence and Bisimulation Join Forces in Probabilistic AutomataYuan Feng, Lijun Zhang. 247-262 [doi]
- Precise Predictive Analysis for Discovering Communication Deadlocks in MPI ProgramsVojtech Forejt, Daniel Kroening, Ganesh Narayanaswamy, Subodh Sharma. 263-278 [doi]
- Proof Patterns for Formal MethodsLeo Freitas, Iain Whiteside. 279-295 [doi]
- Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating SystemHendra Gunadi, Alwen Tiu. 296-311 [doi]
- iscasMc: A Web-Based Probabilistic Model CheckerErnst Moritz Hahn, Yi Li, Sven Schewe, Andrea Turrini, Lijun Zhang. 312-317 [doi]
- Invariants, Well-Founded Statements and Real-Time Program AlgebraIan J. Hayes, Larissa Meinicke. 318-334 [doi]
- Checking Liveness Properties of Presburger Counter Systems Using Reachability AnalysisK. Vasanta Lakshmi, Aravind Acharya, Raghavan Komondoor. 335-350 [doi]
- A Symbolic Algorithm for the Analysis of Robust Timed AutomataPiotr Kordy, Rom Langerak, Sjouke Mauw, Jan Willem Polderman. 351-366 [doi]
- Revisiting Compatibility of Input-Output Modal Transition SystemsIvo Krka, Nicolás D'Ippolito, Nenad Medvidovic, Sebastián Uchitel. 367-381 [doi]
- Co-induction Simply - Automatic Co-inductive Proofs in a Program VerifierK. Rustan M. Leino, Michal Moskal. 382-398 [doi]
- Management of Time Requirements in Component-Based SystemsYi Li, Tian Huat Tan, Marsha Chechik. 399-415 [doi]
- Compositional Synthesis of Concurrent Systems through Causal Model Checking and LearningShang-Wei Lin, Pao-Ann Hsiung. 416-431 [doi]
- Formal Verification of Operational TransformationYang Liu, Yi Xu, Shao Jie Zhang, Chengzheng Sun. 432-448 [doi]
- Verification of a Transactional Memory Manager under Hardware Failures and RestartsOgnjen Maric, Christoph Sprenger. 449-464 [doi]
- SCJ: Memory-Safety Checking without AnnotationsChris Marriott, Ana Cavalcanti. 465-480 [doi]
- Refactoring, Refinement, and Reasoning - A Logical Characterization for Hybrid SystemsStefan Mitsch, Jan-David Quesel, André Platzer. 481-496 [doi]
- Object PropositionsLigia Nistor, Jonathan Aldrich, Stephanie Balzer, Hannes Mehnert. 497-513 [doi]
- Flexible Invariants through Semantic CollaborationNadia Polikarpova, Julian Tschannen, Carlo A. Furia, Bertrand Meyer. 514-530 [doi]
- Efficient Tight Field Bounds Computation Based on Shape PredicatesPablo Ponzio, Nicolás Rosner, Nazareno Aguirre, Marcelo F. Frias. 531-546 [doi]
- A Graph-Based Transformation Reduction to Reach UPPAAL States FasterJonas Rinast, Sibylle Schupp, Dieter Gollmann. 547-562 [doi]
- Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical ComparisonPierre Roux, Pierre-Loïc Garoche. 563-578 [doi]
- Efficient Self-composition for Weakest Precondition CalculiChristoph Scheben, Peter H. Schmitt. 579-594 [doi]
- Towards a Formal Analysis of Information Leakage for Signature Attacks in Preferential ElectionsRoland Wen, Annabelle McIver, Carroll Morgan. 595-610 [doi]
- Analyzing Clinical Practice Guidelines Using a Decidable Metric Interval-Based Temporal LogicMorteza Yousef Sanati, Wendy MacCaull, T. S. E. Maibaum. 611-626 [doi]
- A Modular Theory of Object Orientation in Higher-Order UTPFrank Zeyda, Thiago L. V. L. Santos, Ana Cavalcanti, Augusto Sampaio. 627-642 [doi]
- Formalizing and Verifying a Modern Build LanguageMaria Christakis, K. Rustan M. Leino, Wolfram Schulte. 643-657 [doi]
- The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal VerificationSergio Feo Arenis, Bernd Westphal, Daniel Dietsch, Marco Muñiz, Ahmad Siyar Andisha. 658-672 [doi]
- Formally Verifying Graphics FPU - An Intel® ExperienceAarti Gupta, V. M. Achutha KiranKumar, Rajnish Ghughal. 673-687 [doi]
- MDP-Based Reliability Analysis of an Ambient Assisted Living SystemYan Liu, Lin Gui, Yang Liu. 688-702 [doi]
- Diagnosing Industrial Business Processes: Early ExperiencesSuman Roy, A. S. M. Sajeev, Srivibha Sripathy. 703-717 [doi]
- Formal Verification of Lunar Rover Control Software Using UPPAALLijun Shan, Yuying Wang, Ning Fu, Xingshe Zhou, Lei Zhao, Lijng Wan, Lei Qiao, Jianxin Chen. 718-732 [doi]
- Formal Verification of a Descent Guidance Control Program of a Lunar LanderHengjun Zhao, Mengfei Yang, Naijun Zhan, Bin Gu, Liang Zou, Yao Chen. 733-748 [doi]