César A. Muñoz

94 papers A* 2A 1B 15C 7Misc 3Journal 27Unranked 30

Year	Rank	Type	Title / Venue / Authors
2024	—	`conf`	A Formal Verification Framework for Runtime Assurance. NFM J. Tanner Slagel, Lauren M. White, Aaron Dutle, César A. Muñoz, Nicolas Crespo
2024	B	`conf`	A Temporal Differential Dynamic Logic Formal Embedding. CPP Lauren M. White, Laura Titolo, J. Tanner Slagel, César A. Muñoz
2024	—	`conf`	Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0. FM (2) Laura Titolo, Mariano M. Moscato, Marco A. Feliú, Paolo Masci, César A. Muñoz
2023	—	`conf`	Embedding Differential Dynamic Logic in PVS. LSFA/HCVS J. Tanner Slagel, Mariano M. Moscato, Lauren M. White, César A. Muñoz, Swee Balachandran, Aaron Dutle
2023	—	`ch.`	Floating-Point Round-off Error Analysis of Safety-Critical Avionics Software. Challenges of Software Verification Laura Titolo, Mariano M. Moscato, Marco A. Feliú, Aaron Dutle, César A. Muñoz
2023	J	`jnl`	Formal Verification of Termination Criteria for First-Order Recursive Functions. J. Autom. Reason. César A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, Anthony J. Narkawicz, Ariane Alves Almeida, Andréia B. Avelar da Silva, Thiago Mendonça Ferreira Ramos
2023	J	`jnl`	Selected extended papers of NFM 2021. Innov. Syst. Softw. Eng. Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, Ivan Perez
2022	—	`conf`	Towards an implementation of differential dynamic logic in PVS. SOAP@PLDI J. Tanner Slagel, César A. Muñoz, Swee Balachandran, Mariano M. Moscato, Aaron Dutle, Paolo Masci, Lauren M. White
2021	B	`conf`	Formal Verification of Termination Criteria for First-Order Recursive Functions. ITP César A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, Anthony J. Narkawicz, Ariane Alves Almeida, Andréia B. Avelar, Thiago Mendonça Ferreira Ramos
2021	J	`jnl`	Formal analysis of the compact position reporting algorithm. Formal Aspects Comput. Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, Gregory Anderson, François Bobot
2021	—	`ed.`	NASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings NFM Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, Ivan Perez
2020	—	`conf`	A Graphical Toolkit for the Validation of Requirements for Detect and Avoid Systems. TAP@STAF Paolo Masci, César A. Muñoz
2020	B	`conf`	Automatic Generation of Guard-Stable Floating-Point Code. IFM Laura Titolo, Mariano M. Moscato, Marco A. Feliú, César A. Muñoz
2020	J	`jnl`	Automatic generation and verification of test-stable floating-point code. CoRR Laura Titolo, Mariano M. Moscato, César A. Muñoz
2020	—	`conf`	From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project. FMAS Aaron Dutle, César A. Muñoz, Esther Conrad, Alwyn Goodloe, Laura Titolo, Ivan Perez, Swee Balachandran, Dimitra Giannakopoulou, Anastasia Mavridou, Thomas Pressburger
2019	—	`conf`	A Mixed Real and Floating-Point Solver. NFM Rocco Salvia, Laura Titolo, Marco A. Feliú, Mariano M. Moscato, César A. Muñoz, Zvonimir Rakamaric
2019	—	`conf`	An Integrated Development Environment for the Prototype Verification System. F-IDE@FM Paolo Masci, César A. Muñoz
2019	B	`conf`	Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm. FM Mariano M. Moscato, Laura Titolo, Marco A. Feliú, César A. Muñoz
2019	J	`jnl`	Selected Extended Papers of ITP 2017 - Preface. J. Autom. Reason. Mauricio Ayala-Rincón, César A. Muñoz
2019	J	`jnl`	Selected extended papers of NFM 2018. Innov. Syst. Softw. Eng. Aaron Dutle, César A. Muñoz, Anthony Narkawicz
2018	J	`jnl`	A Decision Procedure for Univariate Polynomial Systems Based on Root Counting and Interval Subdivision. J. Formaliz. Reason. César A. Muñoz, Anthony J. Narkawicz, Aaron Dutle
2018	B	`conf`	A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm. FM Laura Titolo, Mariano M. Moscato, César A. Muñoz, Aaron Dutle, François Bobot
2018	B	`conf`	An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs. VMCAI Laura Titolo, Marco A. Feliú, Mariano M. Moscato, César A. Muñoz
2018	B	`conf`	Boosting the Reuse of Formal Specifications. ITP Mariano M. Moscato, Carlos Gustavo López Pombo, César A. Muñoz, Marco A. Feliú
2018	C	`conf`	Eliminating Unstable Tests in Floating-Point Programs. LOPSTR Laura Titolo, César A. Muñoz, Marco A. Feliú, Mariano M. Moscato
2018	J	`jnl`	Eliminating Unstable Tests in Floating-Point Programs. CoRR Laura Titolo, César A. Muñoz, Marco A. Feliú, Mariano M. Moscato
2018	C	`conf`	Formalization of the Undecidability of the Halting Problem for a Functional Language. WoLLIC Thiago Mendonça Ferreira Ramos, César A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, Anthony Narkawicz
2018	B	`conf`	From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems. FM César A. Muñoz, Anthony Narkawicz, Aaron Dutle
2018	—	`conf`	Inspection of electrical transmission structures with UAV path conformance and lidar-based geofences. ISGT Andrew J. Moore, Matthew Schubert, Nicholas Rymer, Swee Balachandran, Maria Consiglio, César A. Muñoz, Joshua Smith, Dexter Lewis, Paul Schneide
2018	—	`ed.`	NASA Formal Methods - 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings NFM Aaron Dutle, César A. Muñoz, Anthony Narkawicz
2018	J	`jnl`	Selected Extended Papers of NFM 2016: Preface. J. Autom. Reason. César A. Muñoz, Sanjai Rayadurgam, Oksana Tkachuk
2017	—	`conf`	A Formal Analysis of the Compact Position Reporting Algorithm. VSTTE Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz
2017	B	`conf`	Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis. SAFECOMP Mariano M. Moscato, Laura Titolo, Aaron Dutle, César A. Muñoz
2017	B	`ed.`	Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings ITP Mauricio Ayala-Rincón, César A. Muñoz
2017	J	`jnl`	Rewriting modulo SMT and open system analysis. J. Log. Algebraic Methods Program. Camilo Rocha, José Meseguer, César A. Muñoz
2017	—	`conf`	The MINERVA Software Development Process. AFM@NFM Anthony Narkawicz, César A. Muñoz, Aaron Dutle
2016	—	`conf`	Formal Analysis of Extended Well-Clear Boundaries for Unmanned Aircraft. NFM César A. Muñoz, Anthony Narkawicz
2016	—	`ed.`	Proceedings of the Eleventh International Workshop on Developments in Computational Models, DCM 2015, Cali, Colombia, October 28, 2015. DCM César A. Muñoz, Jorge A. Pérez
2016	J	`jnl`	Unmanned aircraft systems in the national airspace system: a formal methods perspective. ACM SIGLOG News César A. Muñoz, Aaron Dutle, Anthony Narkawicz, Jason Upchurch
2015	Misc	`conf`	A Rigorous Generic Branch and Bound Solver for Nonlinear Problems. SYNASC Andrew P. Smith, César A. Muñoz, Anthony J. Narkawicz, Mantas Markevicius
2015	B	`conf`	Affine Arithmetic and Applications to Real-Number Proving. ITP Mariano M. Moscato, César A. Muñoz, Andrew P. Smith
2015	C	`conf`	Formal Methods in Air Traffic Management: The Case of Unmanned Aircraft Systems (Invited Lecture). ICTAC César A. Muñoz
2015	J	`jnl`	Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm's and Tarski's Theorems. J. Autom. Reason. Anthony Narkawicz, César A. Muñoz, Aaron Dutle
2015	—	`conf`	Software Validation via Model Animation. TAP@STAF Aaron Dutle, César A. Muñoz, Anthony Narkawicz, Ricky W. Butler
2014	B	`conf`	Automated Real Proving in PVS via MetiTarski. FM William Denman, César A. Muñoz
2014	C	`conf`	Bifurcation analysis using rigorous branch and bound methods. CCA Andrew P. Smith, Luis G. Crespo, César A. Muñoz, Mark H. Lowenberg
2014	—	`conf`	Rewriting Modulo SMT and Open System Analysis. WRLA Camilo Rocha, José Meseguer, César A. Muñoz
2014	J	`jnl`	Synchronous set relations in rewriting logic. Sci. Comput. Program. Camilo Rocha, César A. Muñoz
2014	B	`conf`	Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol. FM Parasara Sridhar Duggirala, Le Wang, Sayan Mitra, Mahesh Viswanathan, César A. Muñoz
2013	—	`conf`	A Formally Verified Generic Branching Algorithm for Global Optimization. VSTTE Anthony Narkawicz, César A. Muñoz
2013	J	`jnl`	Compositional verification of a communication protocol for a remotely operated aircraft. Sci. Comput. Program. Alwyn Goodloe, César A. Muñoz
2013	J	`jnl`	Formalization of Bernstein Polynomials and Applications to Global Optimization. J. Autom. Reason. César A. Muñoz, Anthony Narkawicz
2013	—	`conf`	Verification of Numerical Programs: From Real Numbers to Floating Point Numbers. NASA Formal Methods Alwyn Goodloe, César A. Muñoz, Florent Kirchner, Loïc Correnson
2012	B	`conf`	A Formal Interactive Verification Environment for the Plan Execution Interchange Language. IFM Camilo Rocha, Héctor Cadavid, César A. Muñoz, Radu Siminiceanu
2012	J	`jnl`	Bounding the Range of a Rational Function over a box. Reliab. Comput. Anthony Narkawicz, Jürgen Garloff, Andrew P. Smith, César A. Muñoz
2012	J	`jnl`	Formal Verification of Conflict Detection Algorithms for Arbitrary Trajectories. Reliab. Comput. Anthony Narkawicz, César A. Muñoz
2012	J	`jnl`	Provably correct conflict prevention bands algorithms. Sci. Comput. Program. Anthony Narkawicz, César A. Muñoz, Gilles Dowek
2011	J	`jnl`	A formal library of set relations and its application to synchronous languages. Theor. Comput. Sci. Camilo Rocha, César A. Muñoz, Gilles Dowek
2011	—	`conf`	Advanced Theorem Proving Techniques in PVS and Applications. LASER Summer School César A. Muñoz, Ramiro A. Demasi
2011	J	`jnl`	Preface: special issue on NASA Formal Methods Symposium 2010. Innov. Syst. Softw. Eng. César A. Muñoz
2011	—	`conf`	Simulation and Verification of Synchronous Set Relations in Rewriting Logic. SBMF Camilo Rocha, César A. Muñoz
2010	—	`conf`	How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project. NASA Formal Methods Ricky W. Butler, George Hagen, Jeffrey Maddalon, César A. Muñoz, Anthony Narkawicz, Gilles Dowek
2010	—	`ed.`	Proceedings International Workshop on Strategies in Rewriting, Proving, and Programming, IWS 2010, Edinburgh, UK, 9th July 2010. IWS Hélène Kirchner, César A. Muñoz
2010	—	`ed.`	Second NASA Formal Methods Symposium - NFM 2010, Washington D.C., USA, April 13-15, 2010. Proceedings NASA Formal Methods César A. Muñoz
2010	J	`jnl`	The proof monad. J. Log. Algebraic Methods Program. Florent Kirchner, César A. Muñoz
2009	C	`conf`	Compositional Verification of a Communication Protocol for a Remotely Operated Vehicle. FMICS Alwyn Goodloe, César A. Muñoz
2009	—	`conf`	Rewriting Logic Semantics of a Plan Execution Language SOS Gilles Dowek, César A. Muñoz, Camilo Rocha
2009	J	`jnl`	Verified Real Number Calculations: A Library for Interval Arithmetic. IEEE Trans. Computers Marc Daumas, David R. Lester, César A. Muñoz
2008	—	`conf`	Experimental Evaluation of a Planning Language Suitable for Formal Verification. MoChArt Radu Siminiceanu, Ricky W. Butler, César A. Muñoz
2008	—	`ed.`	Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings TPHOLs Otmane Aït Mohamed, César A. Muñoz, Sofiène Tahar
2007	C	`conf`	Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm. WoLLIC André Luiz Galdino, César A. Muñoz, Mauricio Ayala-Rincón
2007	—	`ed.`	Proceedings of the 6th International Workshop on Strategies in Automated Deduction, STRATEGIES@IJCAR 2006, Part of PLoC 2006, Seattle, WA, USA, August 16, 2006 STRATEGIES@IJCAR Myla Archer, Thierry Boy de la Tour, César A. Muñoz
2007	J	`jnl`	Verified Real Number Calculations: A Library for Interval Arithmetic CoRR Marc Daumas, David R. Lester, César A. Muñoz
2006	—	`conf`	Formal Analysis of the Operational Concept for the Small Aircraft Transportation System. RODIN Book César A. Muñoz, Victor Carreño, Gilles Dowek
2006	—	`conf`	PVS#: Streamlined Tacticals for PVS. STRATEGIES@IJCAR Florent Kirchner, César A. Muñoz
2006	B	`conf`	Predicate Abstraction of Programs with Non-linear Computation. ATVA Songtao Xia, Ben Di Vito, César A. Muñoz
2006	—	`conf`	Preface. STRATEGIES@IJCAR Myla Archer, Thierry Boy de la Tour, César A. Muñoz
2006	Misc	`conf`	Provably faithful evaluation of polynomials. SAC Sylvie Boldo, César A. Muñoz
2005	A*	`conf`	Automated test generation for engineering applications. ASE Songtao Xia, Ben Di Vito, César A. Muñoz
2005	C	`conf`	Guaranteed Proofs Using Interval Arithmetic. IEEE Symposium on Computer Arithmetic Marc Daumas, Guillaume Melquiond, César A. Muñoz
2005	—	`conf`	Real Number Calculations and Theorem Proving. TPHOLs César A. Muñoz, David R. Lester
2004	A	`conf`	Modeling and verification of an air traffic concept of operations. ISSTA César A. Muñoz, Gilles Dowek, Victor Carreño
2003	J	`jnl`	Formal verification of conflict detection algorithms. Int. J. Softw. Tools Technol. Transf. César A. Muñoz, Victor Carreño, Gilles Dowek, Ricky W. Butler
2003	Misc	`conf`	Simulation and verification I: formal analysis of air traffic management systems: the case of conflict resolution and recovery. WSC Ricky W. Butler, Jeffrey Maddalon, Alfons Geser, César A. Muñoz
2002	—	`ed.`	Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings TPHOLs Victor Carreño, César A. Muñoz, Sofiène Tahar
2001	J	`jnl`	Dependent types and explicit substitutions: a meta-theoretical development. Math. Struct. Comput. Sci. César A. Muñoz
2001	—	`conf`	Formal Verification of Conflict Detection Algorithms. CHARME Ricky W. Butler, Victor Carreño, Gilles Dowek, César A. Muñoz
2001	J	`jnl`	Proof-term synthesis on dependent-type systems via explicit substitutions. Theor. Comput. Sci. César A. Muñoz
2000	—	`conf`	Absolute Explicit Unification. RTA Nikolaj S. Bjørner, César A. Muñoz
2000	—	`conf`	Aircraft Trajectory Modeling and Altering Algorithm Verification. TPHOLs Victor Carreño, César A. Muñoz
2000	J	`jnl`	Explicit Substitions and All That. Rev. Colomb. de Computación Mauricio Ayala-Rincón, César A. Muñoz
1999	—	`conf`	Structural Embeddings: Mechanization with Method. World Congress on Formal Methods César A. Muñoz, John M. Rushby
1996	A*	`conf`	Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus. LICS César A. Muñoz
1996	—	`conf`	Dependent Types with Explicit Substitutiuons: A Meta-theoretical development. TYPES César A. Muñoz