default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID8. NFM 2016: Minneapolis, MN, USA
- Sanjai Rayadurgam, Oksana Tkachuk:
NASA Formal Methods - 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings. Lecture Notes in Computer Science 9690, Springer 2016, ISBN 978-3-319-40647-3
Requirements and Architectures
- Ariane Piel, Jean Bourrely, Stéphanie Lala, Sylvain Bertrand, Romain Kervarc:
Temporal Logic Framework for Performance Analysis of Architectures of Systems. 3-18 - John D. Backes, Michael W. Whalen, Andrew Gacek, John Komp
:
On Implementing Real-Time Specification Patterns Using Observers. 19-33 - Devesh Bhatt, Arunabh Chattopadhyay, Wenchao Li, David Oglesby, Sam Owre, Natarajan Shankar:
Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems. 34-40 - Shalini Ghosh, Daniel Elenius, Wenchao Li, Patrick Lincoln, Natarajan Shankar, Wilfried Steiner:
ARSENAL: Automatic Requirements Specification Extraction from Natural Language. 41-46
Testing and Run-Time Enforcement
- Adam Nellis, Pascal Kesseli, Philippa Ryan Conmy, Daniel Kroening, Peter Schrammel, Michael Tautschnig:
Assisted Coverage Closure. 49-64 - Meng Wu, Haibo Zeng, Chao Wang:
Synthesizing Runtime Enforcer of Safety Properties Under Burst Error. 65-81 - Srinivas Pinisetty, Stavros Tripakis:
Compositional Runtime Enforcement. 82-99 - Hao Ren, Devesh Bhatt, Jan Hvozdovic:
Improving an Industrial Test Generation Tool Using SMT Solver. 100-106 - Hua Zhong, Lingming Zhang, Sarfraz Khurshid:
The comKorat Tool: Unified Combinatorial and Constraint-Based Generation of Structurally Complex Tests. 107-113
Theorem Proving and Proofs
- Susmit Jha, Vasumathi Raman:
Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty. 117-132 - Yi-Chin Wu, Vasumathi Raman, Stéphane Lafortune, Sanjit A. Seshia:
Obfuscator Synthesis for Privacy and Utility. 133-149 - Gaspard Férey, Natarajan Shankar:
Code Generation Using a Formal Model of Reference Counting. 150-165 - Néstor Cataño, Victor Rivera:
EventB2Java: A Code Generator for Event-B. 166-171
Application of Formal Methods
- Albert Rizaldi, Fabian Immler, Matthias Althoff:
A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles. 175-190 - Muhammad Usama Sardar, Nida Afaq, Khaza Anuarul Hoque, Taylor T. Johnson, Osman Hasan:
Probabilistic Formal Verification of the SATS Concept of Operation. 191-205 - Josh Newell, Linna Pang, David Tremaine, Alan Wassyng, Mark Lawford:
Formal Translation of IEC 61131-3 Function Block Diagrams to PVS with Nuclear Application. 206-220 - César A. Muñoz, Anthony Narkawicz:
Formal Analysis of Extended Well-Clear Boundaries for Unmanned Aircraft. 221-226 - Sergio B. Guarro, Ümit Özgüner, Tunc Aldemir, Matt Knudson, Arda Kurt, Michael K. Yau, Mohammad Hejase, Steve Kwon:
Formal Validation and Verification Framework for Model-Based and Adaptive Control Systems. 227-233
Code Generation and Synthesis
- Shaobo He, Shuvendu K. Lahiri, Zvonimir Rakamaric:
Verifying Relative Safety, Accuracy, and Termination for Program Approximations. 237-254 - Jeroen Meijer, Jaco van de Pol:
Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis. 255-271 - Andreas Abel, Jan Reineke:
Gray-Box Learning of Serial Compositions of Mealy Machines. 272-287
Model Checking and Verification
- Clément Fumex, Claire Dross, Jens Gerlach, Claude Marché:
Specification and Proof of High-Level Functional Properties of Bit-Level Programs. 291-306 - Julian Brunner, Peter Lammich:
Formal Verification of an Executable LTL Model Checker with Partial Order Reduction. 307-321 - Jean-Christophe Filliâtre, Mário Pereira:
A Modular Way to Reason About Iteration. 322-336 - Ashlie B. Hocking, Benjamin D. Rodes, John C. Knight, Jack W. Davidson, Clark L. Coleman:
A Proof Infrastructure for Binary Programs. 337-343 - Sidi Mohamed Beillahi, Mohamed Yousri Mahmoud, Sofiène Tahar:
Hierarchical Verification of Quantum Circuits. 344-352
Correctness and Certification
- Michael D. Ernst, Damiano Macedonio, Massimo Merro, Fausto Spoto:
Semantics for Locking Specifications. 355-372 - Jing Liu, John D. Backes, Darren D. Cofer, Andrew Gacek:
From Design Contracts to Component Requirements Verification. 373-387 - Robert P. Goldman, Daniel Bryce, Michael J. S. Pelican, David J. Musliner, Kyungmin Bae:
A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control. 388-394
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 2026-05-27 02:08 CEST 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:
