Automatic Certification of the Active Corner Method for Collision Avoidance

Reference. Automatic Certification of the Active Corner Method for Collision Avoidance

Nishant Kheterpal, J. Tanner Slagel, Elanor Tang, Serra Dane, Jean-Baptiste Jeannin · NFM · 2026 · dynamical-systems · DOI

Cite

Cite as @kheterpal-2026-automatic (helia, typst) · \cite{kheterpal-2026-automatic} (LaTeX)

BibTeX

bibtex · 1 line

@inbook{kheterpal-2026-automatic, title={Automatic Certification of the Active Corner Method for Collision Avoidance}, ISBN={9783032280794}, ISSN={1611-3349}, url={http://dx.doi.org/10.1007/978-3-032-28079-4_25}, DOI={10.1007/978-3-032-28079-4_25}, booktitle={NASA Formal Methods}, publisher={Springer Nature Switzerland}, author={Kheterpal, Nishant and Slagel, J. Tanner and Tang, Elanor and Dane, Serra and Jeannin, Jean-Baptiste}, year={2026}, pages={527–548} }

hayagriva YAML (typst)

yaml · 20 lines

kheterpal-2026-automatic:
  type: chapter
  title: Automatic Certification of the Active Corner Method for Collision Avoidance
  author:
  - Kheterpal, Nishant
  - Slagel, J. Tanner
  - Tang, Elanor
  - Dane, Serra
  - Jeannin, Jean-Baptiste
  date: 2026
  page-range: 527-548
  url: http://dx.doi.org/10.1007/978-3-032-28079-4_25
  serial-number:
    doi: 10.1007/978-3-032-28079-4_25
    isbn: '9783032280794'
    issn: 1611-3349
  parent:
    type: book
    title: NASA Formal Methods
    publisher: Springer Nature Switzerland

Download: kheterpal-2026-automatic.bib · kheterpal-2026-automatic.yml

Cited by (1)

Provably Safe Optimization of Arrival Flows Into Terminal Airspace dane-2026-provablyAIAA AVIATION 2026 Forum · 2026

DOI

Cites 45 works (1 here)

With notes (1)

Automating Geometric Proofs of Collision Avoidance with Active Corners kheterpal-2022-automatingFMCAD · 2022

Avoiding collisions between obstacles and vehicles such as cars, robots or aircraft is essential to the development of automation and autonomy. To simplify the problem, many collision avoidance algorithms and proofs consider vehicles to be a point mass, though the actual vehicles are not points. In this paper, we consider a convex polygonal vehicle with nonzero area traveling along a 2-dimensional trajectory. We derive an easily-checkable, quantifier-free formula to check whether a given obstacle will collide with the vehicle moving on the planned trajectory. We apply our method to two case studies of aircraft collision avoidance and study its performance.

DOI · arXiv

External (44)

NASALib: NASA PVS Library of Formal Developments (2025)
cvc5: A Versatile and Industrial-Strength SMT Solver (2022)
Flexible Proof Production in an Industrial-Strength SMT Solver (2022)
Reconstructing fine-grained proofs of rewrites using a domain-specific language (2022)
Set Propagation Techniques for Reachability Analysis (2021)
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs (2021)
Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant (2021)
Formal verification of semi-algebraic sets and real analytic functions (2021)
PolySafe: A Formally Verified Algorithm for Conflict Detection on a Polynomial Airspace (2020)
Control Barrier Functions: Theory and Applications (2019)
Safe, Aggressive Quadrotor Flight via Reachability-Based Trajectory Design (2019)
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4 (2018)
Hamilton-Jacobi reachability: A brief overview and recent advances (2017)
Proof Certificates in PVS (2017)
SymPy: symbolic computing in Python (2017)
Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis (2017)
An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs (2017)
DO-365: Minimum operational performance standards (MOPS) for detect and avoid (DAA) systems (2017)
Lazy proofs for DPLL(T)-based SMT solvers (2016)
Unmanned aircraft systems in the national airspace system (2016)
Dedukti: a logical framework based on the λΠ-calculus modulo theory (2016)
DAIDALUS: Detect and Avoid Alerting Logic for Unmanned Systems (2015)
Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm’s and Tarski’s Theorems (2015)
Online Verification of Automated Road Vehicles Using Reachability Analysis (2014)
On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles (2013)
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses (2011)
Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL (2011)
Fast LCF-Style Proof Reconstruction for Z3 (2010)
Certification of SAT solvers in Coq (2010)
MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions (2009)
A Brief Overview of PVS (2008)
Batch proving and proof scripting in PVS (Tech. rep.) (2007)
Reachability of Uncertain Linear Systems Using Zonotopes (2005)
Safety Verification of Hybrid Systems Using Barrier Certificates (2004)
Autarkic Computations in Formal Proofs (2002)
Isabelle/HOL: A Proof Assistant for Higher-Order Logic (2002)
PVS prover guide (2001)
Aircraft Trajectory Modeling and Alerting Algorithm Verification (2000)
A certifying compiler for Java (2000)
The design and implementation of a certifying compiler (1998)
PVS: A prototype verification system (1992)
Real quantifier elimination is doubly exponential (1988)
Quantifier elimination for real closed fields by cylindrical algebraic decompostion (1975)
Verification of hybrid systems: formalization and proof rules in PVS