César A. Muñoz

Andréia B. Avelar da Silva

Thiago Mendonça Ferreira Ramos

J. Autom. Reason., December, 2023

Selected extended papers of NFM 2021.

[BibT_eX]

[DOI]

Innov. Syst. Softw. Eng., December, 2023

2022

Towards an implementation of differential dynamic logic in PVS.

[BibT_eX]

[DOI]

Proceedings of the SOAP '22: 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, 2022

2021

Formal analysis of the compact position reporting algorithm.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2021

2020

From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project.

[BibT_eX]

[DOI]

Dimitra Giannakopoulou

Anastasia Mavridou

Thomas Pressburger

Proceedings of the Proceedings Second Workshop on Formal Methods for Autonomous Systems, 2020

Automatic generation and verification of test-stable floating-point code.

[BibT_eX]

[DOI]

Laura Titolo

CoRR, 2020

A Graphical Toolkit for the Validation of Requirements for Detect and Avoid Systems.

[BibT_eX]

[DOI]

Paolo Masci

Proceedings of the Tests and Proofs - 14th International Conference, 2020

Automatic Generation of Guard-Stable Floating-Point Code.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 16th International Conference, 2020

2019

Selected Extended Papers of ITP 2017 - Preface.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

Selected extended papers of NFM 2018.

[BibT_eX]

[DOI]

Innov. Syst. Softw. Eng., 2019

An Integrated Development Environment for the Prototype Verification System.

[BibT_eX]

[DOI]

Paolo Masci

Proceedings of the Proceedings Fifth Workshop on Formal Integrated Development Environment, 2019

A Mixed Real and Floating-Point Solver.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 11th International Symposium, 2019

Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

2018

A Decision Procedure for Univariate Polynomial Systems Based on Root Counting and Interval Subdivision.

[BibT_eX]

[DOI]

Anthony J. Narkawicz

J. Formaliz. Reason., 2018

Selected Extended Papers of NFM 2016: Preface.

[BibT_eX]

[DOI]

Thiago Mendonça Ferreira Ramos

Sanjai Rayadurgam

Oksana Tkachuk

J. Autom. Reason., 2018

Formalization of the Undecidability of the Halting Problem for a Functional Language.

[BibT_eX]

[DOI]

Proceedings of the Logic, Language, Information, and Computation, 2018

An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

Eliminating Unstable Tests in Floating-Point Programs.

[BibT_eX]

[DOI]

Proceedings of the Logic-Based Program Synthesis and Transformation, 2018

Boosting the Reuse of Formal Specifications.

[BibT_eX]

[DOI]

Carlos Gustavo López Pombo

Marco A. Feliú

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Inspection of electrical transmission structures with UAV path conformance and lidar-based geofences.

[BibT_eX]

[DOI]

Proceedings of the 2018 IEEE Power & Energy Society Innovative Smart Grid Technologies Conference, 2018

A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - 22nd International Symposium, 2018

From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - 22nd International Symposium, 2018

2017

Rewriting modulo SMT and open system analysis.

[BibT_eX]

[DOI]

José Meseguer

J. Log. Algebraic Methods Program., 2017

A Formal Analysis of the Compact Position Reporting Algorithm.

[BibT_eX]

[DOI]

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2017

Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, Reliability, and Security, 2017

The MINERVA Software Development Process.

[BibT_eX]

[DOI]

Proceedings of the Automated Formal Methods, 2017

2016

Unmanned aircraft systems in the national airspace system: a formal methods perspective.

[BibT_eX]

[DOI]

ACM SIGLOG News, 2016

Formal Analysis of Extended Well-Clear Boundaries for Unmanned Aircraft.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

2015

Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm's and Tarski's Theorems.

[BibT_eX]

[DOI]

J. Autom. Reason., 2015

Software Validation via Model Animation.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 9th International Conference, 2015

A Rigorous Generic Branch and Bound Solver for Nonlinear Problems.

[BibT_eX]

[DOI]

Proceedings of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2015

Affine Arithmetic and Applications to Real-Number Proving.

[BibT_eX]

[DOI]

Andrew P. Smith

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Formal Methods in Air Traffic Management: The Case of Unmanned Aircraft Systems (Invited Lecture).

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2015, 2015

2014

Synchronous set relations in rewriting logic.

[BibT_eX]

[DOI]

Parasara Sridhar Duggirala

Sci. Comput. Program., 2014

Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol.

[BibT_eX]

[DOI]

Proceedings of the FM 2014: Formal Methods, 2014

Automated Real Proving in PVS via MetiTarski.

[BibT_eX]

[DOI]

William Denman

Proceedings of the FM 2014: Formal Methods, 2014

Bifurcation analysis using rigorous branch and bound methods.

[BibT_eX]

[DOI]

Proceedings of the 2014 IEEE Conference on Control Applications, 2014

2013

Compositional verification of a communication protocol for a remotely operated aircraft.

[BibT_eX]

[DOI]

Alwyn Goodloe

Sci. Comput. Program., 2013

Formalization of Bernstein Polynomials and Applications to Global Optimization.

[BibT_eX]

[DOI]

J. Autom. Reason., 2013

A Formally Verified Generic Branching Algorithm for Global Optimization.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Verification of Numerical Programs: From Real Numbers to Floating Point Numbers.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods, 2013

2012

Provably correct conflict prevention bands algorithms.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2012

Formal Verification of Conflict Detection Algorithms for Arbitrary Trajectories.

[BibT_eX]

[DOI]

Reliab. Comput., 2012

Bounding the Range of a Rational Function over a box.

[BibT_eX]

[DOI]

Reliab. Comput., 2012

A Formal Interactive Verification Environment for the Plan Execution Interchange Language.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 9th International Conference, 2012

2011

A formal library of set relations and its application to synchronous languages.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2011

Preface: special issue on NASA Formal Methods Symposium 2010.

[BibT_eX]

[DOI]

Innov. Syst. Softw. Eng., 2011

Simulation and Verification of Synchronous Set Relations in Rewriting Logic.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods, Foundations and Applications - 14th Brazilian Symposium, 2011

Advanced Theorem Proving Techniques in PVS and Applications.

[BibT_eX]

[DOI]

Ramiro A. Demasi

Proceedings of the Tools for Practical Software Verification, 2011

2010

The proof monad.

[BibT_eX]

[DOI]

Florent Kirchner

J. Log. Algebraic Methods Program., 2010

How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project.

[BibT_eX]

Proceedings of the Second NASA Formal Methods Symposium, 2010

2009

Verified Real Number Calculations: A Library for Interval Arithmetic.

[BibT_eX]

[DOI]

Marc Daumas

David R. Lester

IEEE Trans. Computers, 2009

Rewriting Logic Semantics of a Plan Execution Language

[BibT_eX]

[DOI]

Proceedings of the Proceedings Sixth Workshop on Structural Operational Semantics, 2009

Compositional Verification of a Communication Protocol for a Remotely Operated Vehicle.

[BibT_eX]

[DOI]

Alwyn Goodloe

Proceedings of the Formal Methods for Industrial Critical Systems, 2009

2008

Experimental Evaluation of a Planning Language Suitable for Formal Verification.

[BibT_eX]

[DOI]

Radu Siminiceanu

Ricky W. Butler

Proceedings of the Model Checking and Artificial Intelligence, 5th International Workshop, 2008

2007

Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm.

[BibT_eX]

[DOI]

André Luiz Galdino

Proceedings of the Logic, 2007

2006

PVS#: Streamlined Tacticals for PVS.

[BibT_eX]

[DOI]

Florent Kirchner

Proceedings of the 6th International Workshop on Strategies in Automated Deduction, 2006

Preface.

[BibT_eX]

[DOI]

Myla Archer

Thierry Boy de la Tour

Proceedings of the 6th International Workshop on Strategies in Automated Deduction, 2006

Provably faithful evaluation of polynomials.

[BibT_eX]

[DOI]

Sylvie Boldo

Proceedings of the 2006 ACM Symposium on Applied Computing (SAC), 2006

Formal Analysis of the Operational Concept for the Small Aircraft Transportation System.

[BibT_eX]

[DOI]

Victor Carreño

Proceedings of the Rigorous Development of Complex Fault-Tolerant Systems [FP6 IST-511599 RODIN project], 2006

Predicate Abstraction of Programs with Non-linear Computation.

[BibT_eX]

[DOI]

Songtao Xia

Ben Di Vito

Proceedings of the Automated Technology for Verification and Analysis, 2006

2005

Real Number Calculations and Theorem Proving.

[BibT_eX]

[DOI]

David R. Lester

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Automated test generation for engineering applications.

[BibT_eX]

[DOI]

Songtao Xia

Ben Di Vito

Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering (ASE 2005), 2005

Guaranteed Proofs Using Interval Arithmetic.

[BibT_eX]

[DOI]

Marc Daumas

Guillaume Melquiond

Proceedings of the 17th IEEE Symposium on Computer Arithmetic (ARITH-17 2005), 2005

2004

Modeling and verification of an air traffic concept of operations.

[BibT_eX]

[DOI]

Victor Carreño

Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2004

2003

Formal verification of conflict detection algorithms.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2003

Simulation and verification I: formal analysis of air traffic management systems: the case of conflict resolution and recovery.

[BibT_eX]

[DOI]

Proceedings of the 35th Winter Simulation Conference: Driving Innovation, 2003

2001

Proof-term synthesis on dependent-type systems via explicit substitutions.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2001

Dependent types and explicit substitutions: a meta-theoretical development.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2001

2000

Explicit Substitions and All That.

[BibT_eX]

[DOI]

Rev. Colomb. de Computación, 2000

Aircraft Trajectory Modeling and Altering Algorithm Verification.

[BibT_eX]

[DOI]

Victor Carreño

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

Absolute Explicit Unification.

[BibT_eX]

[DOI]

Nikolaj S. Bjørner

Proceedings of the Rewriting Techniques and Applications, 11th International Conference, 2000

1999

Structural Embeddings: Mechanization with Method.

[BibT_eX]

[DOI]

John M. Rushby

Proceedings of the FM'99 - Formal Methods, 1999

1996

Dependent Types with Explicit Substitutiuons: A Meta-theoretical development.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, 1996

Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus.

[BibT_eX]

[DOI]