NFM 2010

Accepted Papers

The program committee selected 20 regular papers and 4 short papers from over 50 submissions. Each paper was read by 4 reviewers.

Selected papers published in Innovations in Systems and Software Engineering: Special Issue NFM 2010, Volume 7, Issue 2, 2011 (BibTex).

Proceedings of the Second NASA Formal Methods Symposium appear as NASA Conference Publication NASA/CP-2010-216215, 2010 (BibTex).

(Show abstracts)

Regular Papers

• Paolo Arcaini, Angelo Gargantini and Elvinia Riccobene. Automatic Review of Abstract State Machines by Meta Property Verification (Abstract, Talk, BibTex)
• Sylvie Boldo Thi Minh and Tuyen Nguyen. Hardware-independent Proofs of Numerical Programs (Abstract, Talk, BibTex)
• Andreas Bollin. Slice-based Formal Specification Measures - Mapping Coupling and Cohesion Measures to Formal Z (Abstract, Talk, BibTex)
• Ricky Butler, George Hagen, Jeffrey Maddalon, César Muñoz, Anthony Narkawicz and Gilles Dowek. How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project (Abstract, Talk, BibTex)
• Nestor Cataño and Radu Siminiceanu. A Machine-Checked Proof of A State-Space Construction Algorithm (Abstract, Talk, BibTex)
• Sagar Chaki and Arie Gurfinkel. Automated Assume-Guarantee Reasoning for Omega-Regular Systems and Specifications (Abstract, Talk, BibTex)
• Xiang Fu and Chung-Chih Li. Modeling Regular Replacement for String Constraint Solving (Abstract, Talk, BibTex)
• Xiaowan Huang, Anu Singh and Scott A. Smolka. Using Integer Clocks to Verify the Timing-Sync Sensor Network Protocol (Abstract, Talk, BibTex)
• Eduardo Rafael López Ruiz and Michel Lemoine. Can Regulatory Bodies Expect Efficient Help from Formal Methods? (Abstract, Talk, BibTex)
• Srinivas Nedunuri, Douglas R. Smith and William R. Cook. Synthesis of Greedy Algorithms Using Dominance Relations (Abstract, Talk, BibTex)
• Lehilton L. C. Pedrosa and Arnaldo V. Moura. A New Method for Incremental Testing of Finite State Machines (Abstract, Talk, BibTex)
• Concetta Pilotto and Jerome White. Verification of Faulty Message Passing Systems with Continuous State Space in PVS (Abstract, Talk, BibTex)
• Petra Price and Greg Turgeon. Phase Two Feasibility Study for Software Safety Requirements Analysis Using Model Checking (Abstract, Talk, BibTex)
• Dominic Richards and David Lester. A Prototype Embedding of Bluespec SystemVerilog in the PVS Theorem Prover (Abstract, Talk, BibTex)
• Pritam Roy and Natarajan Shankar. SimCheck: An Expressive Type System for Simulink (Abstract, Talk, BibTex)
• Matt Staats, Michael Whalen, Ajitha Rajan and Mats Heimdahl. Coverage Metrics for Requirements-Based Testing: Evaluation of Effectiveness (Abstract, Talk, BibTex)
• Sarah Thompson, Guillaume Brat and Arnaud Venet. Software Model Checking of ARINC-653 Flight Code with MCP (Abstract, BibTex)
• Sanaz Yeganefard, Michael Butler and Abdolbaghi Rezazadeh. Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B (Abstract, Talk, BibTex)
• Xiang Yin and John Knight. Formal Verification of Large Software Systems (Abstract, Talk, BibTex)
• Yang Zhao and Gianfranco Ciardo. Symbolic Computation of Strongly Connected Components Using Saturation (Abstract, Talk, BibTex)

Short Papers

• Erik Endres, Christian Müller, Andrey Shadrin and Sergey Tverdyshev. Towards the Formal Verification of a Distributed Real-Time Automotive System (Abstract, Talk, BibTex)
• Viet Yen Nguyen, Thomas Noll and Max Odenbrett. Slicing AADL Specifications for Model Checking (Abstract, Talk, BibTex)
• Pierre Roux and Radu Siminiceanu. Model Checking with Edge-valued Decision Diagrams (Abstract, Talk, BibTex)
• Christian Saad and Bernhard Bauer. Data-flow Based Model Analysis (Abstract, Talk, BibTex)