Research

Publications [DPLB]

AAS TP	A formally verified hybrid system for the next-generation airborne collision avoidance system	TACAS	2015	[pdf \| talk \| bib \| techreport \| springer]
TP	A hierarchy of proof rules for checking differential invariance of algebraic sets	VMCAI	2015	[pdf \| talk \| bib \| techreport \| benchmarks \| springer]
RAG TP	Invariance of conjunctions of polynomial equalities for algebraic differential equations	SAS	2014	[pdf \| talk \| bib \| techreport \| benchmarks \| springer]
RAG AI TP	Characterizing algebraic invariants by differential radical invariants	TACAS	2014	[pdf \| talk \| bib \| techreport \| springer]
AAS TP	Hybrid theorem proving of aerospace systems: Applications and challenges	JAIS	2014	[pdf \| talk \| bib \| jais]
TP	On provably safe obstacle avoidance for autonomous robotic ground vehicles	RSS	2013	[pdf \| talk \| bib \| rss]
CA AI	Donut domains: Efficient non-convex domains for abstract interpretation	VMCAI	2012	[pdf \| talk \| bib \| springer]
MC	Efficient probabilistic model checking of systems with ranged probabilities	RP	2012	[pdf \| talk \| bib \| springer]
CA AI	A logical product approach to zonotope intersection	CAV	2010	[pdf \| talk \| bib \| arXiv \| springer]
AI	The zonotope abstract domain Taylor1+	CAV	2009	[pdf \| talk \| bib \| springer]
AAS AI	Space software validation using abstract interpretation	DASIA	2009	[pdf \| talk \| bib \| dasia]

Thomas Heinz	Bosch, Germany
André Platzer	CMU, PA, USA
Erik Zawadski	CMU, PA, USA
Jean-Baptiste Jeannin	CMU, PA, USA
Stefan Mitsch	CMU, PA, USA
Franz Franchetti	CMU, PA, USA
Eric Goubault	CNRS/Ecole Polytechnique, France
Sylvie Putot	CNRS/Ecole Polytechnique, France
David Lesens	EADS, Astrium ST, France
Gogul Balakrishnan	Google Inc., CA, USA
Vineet Kahlon	Google Inc., CA, USA
Franjo Ivancic	Google Inc., NY, USA
Aurora Schmidt	JHU/APL, MD, USA
Ryan Gardner	JHU/APL, MD, USA
Yanni Kouskoulas	JHU/APL, MD, USA
Olivier Bouissou	Mathworks, France
Aarti Gupta	NEC-Labs, NJ, USA
Parasara Sridhar Duggirala	UIUC, IL, USA
Andrew Sogokon	University of Edinburgh, Scotland, UK

AI	Abstract Interpretation
TP	Theorem Proving
MC	Model Checking
AAS	Formal Verification of Avionic and Aerospace Systems
CA	Convex Analysis
RAG	Real Algebraic Geometry