Formal Verification and Automated Testing for Diagnostic and Monitoring Systems (2009)
Bruno Dutertre, John Rushby, Ashish Tiwari, César Muñoz, Radu Siminiceanu
Formal methods offer the unique benefit that it is possible to examine all possible circumstances within a given scope, rather than merely sample them as with testing and simulation. This is possible...
PVS#: Streamlined Tacticals for PVS 1 (2008)
Replace this file with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting. Both can be
A Formal Analysis Framework for PLEXIL (2008)
Gilles Dowek, César Muñoz, Corina S. Păsăreanu
The Plan Execution Interchange Language (PLEXIL) is a rich concurrent and reactive language developed by NASA to support autonomous commanding and monitoring for a variety of space systems. In this...
Safety Verification of the Small Aircraft Transportation System Concept of Operations (2008)
A critical factor in the adoption of any new aeronautical technology or concept of operation is safety. Traditionally, safety verification is accomplished through a rigorous process that involves...
General Terms Verification, Theory (2008)
Songtao Xia, Ben Di Vito, César Muñoz
In test generation based on model-checking, white-box test criteria are represented as trap conditions written in a temporal logic. A model checker is used to refute trap conditions with...
PVS#: Streamlined Tacticals for PVS 1 (2008)
The semantics of a proof language relies on the representation of the state of a proof after a logical rule has been applied. This information, which is usually meaningless from a logical point of...
Verified Real Number Calculations: A Library for Interval Arithmetic (2007)
Daumas, Marc, Lester, David, Muñoz, César
Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or...
Verified Real Number Calculations: A Library for Interval Arithmetic (2007)
Daumas, Marc, Lester, David, Muñoz, César
Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or...
Verified Real Number Calculations: A Library for Interval Arithmetic (2007)
Daumas, Marc, Lester, David, Muñoz, César
Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or...
M.: Formal verification of an optimal air traffic conflict resolution and recovery algorithm (2007)
André L. Galdino, César Muñoz, Mauricio Ayala-rincón
Abstract. Highly accurate positioning systems and new broadcasting technology have enabled air traffic management concepts where the responsibility for aircraft separation resides on pilots rather...
André Luiz Galdino, César A. Muñoz, Kbd André, Luiz Galdino, Kbd André, ...
Three Dimensional conflict detection and resolution algorithm (CD&R) which allows either changes of vertical speed only or of horizontal speed only or of heading only. KB2D- Two Dimensional...
Provably Faithful Evaluation of Polynomials (2005)
We provide sufficient conditions that formally guarantee that the floating-point computation of a polynomial evaluation is faithful. To this end, we develop a formalization of floating-point numbers...
Provably Faithful Evaluation of Polynomials (2005)
We provide sufficient conditions that formally guarantee that the floating-point computation of a polynomial evaluation is faithful. To this end, we develop a formalization of floating-point numbers...
Provably Faithful Evaluation of Polynomials (2005)
We provide sufficient conditions that formally guarantee that the floating-point computation of a polynomial evaluation is faithful. To this end, we develop a formalization of floating-point numbers...
Guaranteed Proofs Using Interval Arithmetic (2005)
Daumas, Marc, Melquiond, Guillaume, Muñoz, César
This paper presents a set of tools for mechanical reasoning of numerical bounds using interval arithmetic. The tools implement two techniques for reducing decorrelation: interval splitting and...
Guaranteed Proofs Using Interval Arithmetic (2005)
Daumas, Marc, Melquiond, Guillaume, Muñoz, César
This paper presents a set of tools for mechanical reasoning of numerical bounds using interval arithmetic. The tools implement two techniques for reducing decorrelation: interval splitting and...
NASA/TP–2004–213015 Formal Verification of a Conflict Resolution and Recovery Algorithm (2004)
Jeffrey Maddalon, Ricky Butler, Alfons Geser, César Muñoz
Since its founding, NASA has been dedicated to the advancement of aeronautics and space science. The NASA Scientific and Technical Information (STI) Program Office plays a key part in helping NASA...
NASA/TP–2004–213015 Formal Verification of a Conflict Resolution and Recovery Algorithm (2004)
Jeffrey Maddalon, Ricky Butler, Alfons Geser, César Muñoz
Since its founding, NASA has been dedicated to the advancement of aeronautics and space science. The NASA Scientific and Technical Information (STI) Program Office plays a key part in helping NASA...
Formal verification of conflict detection algorithms (2001)
Ricky Butler, Víctor Carreño, Gilles Dowek, César Muñoz
Abstract. Safety assessment of new air traffic management systems is a main issue for civil aviation authorities. Standard techniques such as testing and simulation have serious limitations in new...
Aircraft trajectory modeling and alerting algorithm verification (2000)
César Muñoz, Victor Carreño, Cesar Mu, Victor Carre No
Abstract. The Airborne Information for Lateral Spacing (AILS) program at NASA Langley Research Center aims at giving pilots the information necessary to make independent approaches to parallel...
Towards a Customizable PVS (2000)
Gerald Lüttgen, César Muñoz, Ricky Butler, Ben Di Vito, Paul Miner, Gerald Luttgen Y, ...
PVS is a state-of-the-art theorem-proving tool developed by SRI International. It is used inavariety of academic and real-world applications by NASA and ICASE researchers, for whom tool customization...
Absolute Explicit Unification (2000)
. This paper presents a system for explicit substitutions in Pure Type Systems (PTS). The system allows to solve type checking, type inhabitation, higher-order unification, and type inference for PTS...
Structural Embeddings: Mechanization with Method (1999)
. The most powerful tools for analysis of formal specifications are general-purpose theorem provers and model checkers, but these tools provide scant methodological support. Conversely, those...
PBS: Support for the B-Method in PVS (1999)
The B-method is a state-oriented formal method for software development. It provides a uniform language, the abstract machine notation, to specify, design, and implement systems. The underlying logic...
Structural Embeddings: Mechanization with Method (1999)
. The most powerful tools for analysis of formal specifications are general-purpose theorem provers and model checkers such as PVS and SMV, but these tools provide scant methodological support,...
) C'esar Mu~noz Computer Science Laboratory SRI International 333 Ravenswood Avenue Menlo Park, CA 94025, USA Email: munoz@csl.sri.com Tel: +1 (650) 859-2784, Fax: +1 (650) 859-2844 February 24,...
The Coq Proof Assistant Reference Manual : Version 6.1 (1997)
Barras, Bruno, Boutin, Samuel, Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Giménez, Eduardo, ...
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. Coq V6.1 is available by anonymous ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.1 and...
A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory (1997)
In the framework of intuitionnistic logic and type theory, the concepts of «propositions» and «types» are identified. This principle is known as the Curry-Howard isomorphism, and it is at the...
The Coq Proof Assistant Reference Manual : Version 6.1 (1997)
Barras, Bruno, Boutin, Samuel, Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Giménez, Eduardo, ...
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. Coq V6.1 is available by anonymous ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.1 and...
Meta-Theoretical Properties of lambda_phi: A Left-Linear Variant of lambda_sigma (1997)
In this paper we consider explicit substitutions calculi that allow open terms. In particular, we propose a variant of the $\lambda_\sigma$-calculus, that we call $\lambda_\phi$. For this calculus...
A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory (1997)
In the framework of intuitionnistic logic and type theory, the concepts of «propositions» and «types» are identified. This principle is known as the Curry-Howard isomorphism, and it is at the...
The Coq Proof Assistant Reference Manual : Version 6.1 (1997)
Barras, Bruno, Boutin, Samuel, Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Giménez, Eduardo, ...
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. Coq V6.1 is available by anonymous ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.1 and...
Meta-Theoretical Properties of lambda_phi: A Left-Linear Variant of lambda_sigma (1997)
In this paper we consider explicit substitutions calculi that allow open terms. In particular, we propose a variant of the $\lambda_\sigma$-calculus, that we call $\lambda_\phi$. For this calculus...
Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus (1996)
César Muñoz, Inria Rocquencourt
Explicit substitutions calculi are formal systems that implement fi-reduction by means of an internal substitution operator. In that calculi it is possible to delay the application of a substitution...
The Coq Proof Assistant - Reference Manual V 5.10 (1995)
Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Gérard Huet, Chetan Murthy, César Muñoz, ...
ion All Axiom Begin Cd Chapter Check CheckGuard CoFixpoint Compute Defined Definition Drop Elimination End Eval Explain Extraction Fact Fixpoint Focus for Go Goal Hint Hypothesis Immediate Induction...