Fetching the paper…
Reading the bibliography…
Verified artificial intelligence (AI) is the goal of designing AI-based systems that that have strong, ideally provable, assurances of correctness with respect to mathematically-specified requirements.
Design and synthesis of synchronization skeletons using branching-time temporal logic
Edmund M. Clarke and E. Allen Emerson · 1981
Earlier work this paper cites.
Specification and verification of concurrent systems in CESAR
Jean-Pierre Queille and Joseph Sifakis · 1982
Earlier work this paper cites.
Graph-based algorithms for Boolean function manipulation
Randal E. Bryant · 1986
Earlier work this paper cites.
Explanation-based generalization: A unifying view
Tom M Mitchell, Richard M Keller, and Smadar T Kedar-Cabelli · 1986
Earlier work this paper cites.
On the synthesis of a reactive module
Amir Pnueli and Roni Rosner · 1989
Earlier work this paper cites.
Bounded rationality
Herbert A Simon · 1990
Earlier work this paper cites.
A specifier’s introduction to formal methods
Jeannette M Wing · 1990
Earlier work this paper cites.
PVS: A prototype verification system
S. Owre, J. M. Rushby, and N. Shankar · 1992
Earlier work this paper cites.
Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic
M. J. C. Gordon and T. F. Melham · 1993
Earlier work this paper cites.
Formal methods: State of the art and future directions
Edmund M Clarke and Jeannette M Wing · 1996
Earlier work this paper cites.
Machine Learning
Tom M. Mitchell · 1997
Earlier work this paper cites.
Rationality and intelligence
Stuart J Russell · 1997
Earlier work this paper cites.
Model Checking
Edmund M. Clarke, Orna Grumberg, and Doron A. Peled · 2000
Earlier work this paper cites.
Dynamically Discovering Likely Program Invariants
Michael Ernst · 2000
Earlier work this paper cites.
Computer-Aided Reasoning: An Approach
Matt Kaufmann, Panagiotis Manolios, and J. Strother Moore · 2000
Earlier work this paper cites.
Algorithms for inverse reinforcement learning
Andrew Y. Ng and Stuart J. Russell · 2000
Earlier work this paper cites.
Efficient detection of vacuity in ACTL formulas
I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh · 2001
Earlier work this paper cites.
Using simplicity to control complexity
Lui Sha · 2001
Earlier work this paper cites.
Using model checking to help discover mode confusions and other automation surprises
John Rushby · 2002
Earlier work this paper cites.
Computational techniques for the verification of hybrid systems
Claire Tomlin, Ian Mitchell, Alexandre M. Bayen, and Meeko Oishi · 2003
Earlier work this paper cites.
Monitoring temporal properties of continuous signals
Oded Maler and Dejan Nickovic · 2004
Earlier work this paper cites.
Robust Control of Markov Decision Processes with Uncertain Transition Matrices
A. Nilim and L. El Ghaoui · 2005
Earlier work this paper cites.
Combinatorial sketching for finite programs
Armando Solar-Lezama, Liviu Tancau, Rastislav Bodík, Sanjit A. Seshia, and Vijay A. Saraswat · 2006
Earlier work this paper cites.
Stimulus generation for constrained random simulation
Nathan Kitchen and Andreas Kuehlmann · 2007
Earlier work this paper cites.
Blog: Probabilistic models with unknown objects
Brian Milch, Bhaskara Marthi, Stuart Russell, David Sontag, Daniel L Ong, and Andrey Kolobov · 2007
Earlier work this paper cites.
Satisfiability modulo theories
Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli · 2009
Earlier work this paper cites.
Applied Assertion-Based Verification: An Industry Perspective
Harry Foster · 2009
Earlier work this paper cites.
Boolean satisfiability: From theoretical hardness to practical success
Sharad Malik and Lintao Zhang · 2009
Earlier work this paper cites.
Quantitative languages
Krishnendu Chatterjee, Laurent Doyen, and Thomas A Henzinger · 2010
Earlier work this paper cites.
Artificial intelligence: a modern approach
Stuart Jonathan Russell and Peter Norvig · 2010
Cited alongside, same era.
PRISM 4.0: Verification of probabilistic real-time systems
Marta Kwiatkowska, Gethin Norman, and David Parker · 2011
Cited alongside, same era.
Taming Dr. Frankenstein: Contract-based design for cyber-physical systems
Alberto Sangiovanni-Vincentelli, Werner Damm, and Roberto Passerone · 2012
Cited alongside, same era.
Sciduction: Combining induction, deduction, and structure for verification and synthesis
Sanjit A. Seshia · 2012
Cited alongside, same era.
Polynomial-time verification of PCTL properties of MDPs with convex uncertainties
Alberto Puggelli, Wenchao Li, Alberto Sangiovanni-Vincentelli, and Sanjit A. Seshia · 2013
Cited alongside, same era.
Reachability-based safe learning with Gaussian processes
Anayo K Akametalu, Jaime F Fisac, Jeremy H Gillula, Shahab Kaynama, Melanie N Zeilinger, and Claire J Tomlin · 2014
Combining model checking and runtime verification for safe robotics
Ankush Desai, Tommaso Dreossi, and Sanjit A. Seshia · 2017
Closest in time.
Compositional falsification of cyber-physical systems with machine learning components
Tommaso Dreossi, Alexandre Donze, and Sanjit A. Seshia · 2017
Closest in time.
Safety verification of deep neural networks
Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu · 2017
Closest in time.
A Theory of Formal Synthesis via Inductive Learning
Susmit Jha and Sanjit A. Seshia · 2017
Closest in time.
Developing bug-free machine learning systems with formal mathematics
Daniel Selsam, Percy Liang, and David L. Dill · 2017
Closest in time.
Compositional verification without compositional specification for learning-based systems
Sanjit A. Seshia · 2017
Closest in time.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
Automatic exploit generation
Thanassis Avgerinos, Sang Kil Cha, Alexandre Rebert, Edward J. Schwartz, Maverick Woo, and David Brumley · 2014
Cited alongside, same era.
Distribution-aware sampling and weighted model counting for SAT
Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, and Moshe Y. Vardi · 2014
Cited alongside, same era.
Specification Mining: New Formalisms, Algorithms and Applications
Wenchao Li · 2014
Cited alongside, same era.
Synthesis for human-in-the-loop control systems
Wenchao Li, Dorsa Sadigh, S. Shankar Sastry, and Sanjit A. Seshia · 2014
Cited alongside, same era.
Data-driven probabilistic modeling and verification of human driver behavior
Dorsa Sadigh, Katherine Driggs-Campbell, Alberto Puggelli, Wenchao Li, Victor Shia, Ruzena Bajcsy, Alberto L. Sangiovanni-Vincentelli, S. Shankar Sastry, and Sanjit A. Seshia · 2014
Cited alongside, same era.
ν \nu z-an optimizing SMT solver
Nikolaj Bjørner, Anh-Dung Phan, and Lars Fleckenstein · 2015
Cited alongside, same era.
Smc: Satisfiability modulo convex optimization
Yasser Shoukry, Pierluigi Nuzzo, Alberto Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, and Paulo Tabuada · 2017
Closest in time.
Logical clustering and learning for time-series data
Marcell Vazquez-Chanlatte, Jyotirmoy V. Deshmukh, Xiaoqing Jin, and Sanjit A. Seshia · 2017
Closest in time.
Semantic adversarial deep learning
Tommaso Dreossi, Somesh Jha, and Sanjit A. Seshia · 2018
Closest in time.
A general safety framework for learning-based control in uncertain robotic systems
Jaime F Fisac, Anayo K Akametalu, Melanie N Zeilinger, Shahab Kaynama, Jeremy Gillula, and Claire J Tomlin · 2018
Closest in time.
AI2: Safety and robustness certification of neural networks with abstract interpretation
Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev · 2018
Closest in time.
Making machine learning robust against adversarial inputs
Ian Goodfellow, Patrick McDaniel, and Nicolas Papernot · 2018
Closest in time.
Differentiable monte carlo ray tracing through edge sampling
Tzu-Mao Li, Miika Aittala, Frédo Durand, and Jaakko Lehtinen · 2018
Closest in time.
Formal specification for deep neural networks
Sanjit A. Seshia, Ankush Desai, Tommaso Dreossi, Daniel Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, and Xiangyu Yue · 2018
Closest in time.
Learning task specifications from demonstrations
Marcell Vazquez-Chanlatte, Susmit Jha, Ashish Tiwari, Mark K. Ho, and Sanjit A. Seshia · 2018
Closest in time.
A semantic loss function for deep learning with symbolic knowledge
Jingyi Xu, Zilu Zhang, Tal Friedman, Yitao Liang, and Guy Van den Broeck · 2018
Closest in time.
An overview of machine teaching
Xiaojin Zhu, Adish Singla, Sandra Zilles, and Anna N Rafferty · 2018
Closest in time.
Liability, ethics, and culture-aware behavior specification using rulebooks
Andrea Censi, Konstantin Slutsky, Tichakorn Wongpiromsarn, Dmitry Yershov, Scott Pendleton, James Fu, and Emilio Frazzoli · 2019
Closest in time.
A runtime assurance framework for programming safe robotics systems
Ankush Desai, Shromona Ghosh, Sanjit A. Seshia, Natarajan Shankar, and Ashish Tiwari · 2019
Closest in time.
VerifAI: A toolkit for the formal design and analysis of artificial intelligence-based systems
Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, and Sanjit A. Seshia · 2019
Closest in time.
A formalization of robustness for deep neural networks
Tommaso Dreossi, Shromona Ghosh, Alberto L. Sangiovanni-Vincentelli, and Sanjit A. Seshia · 2019
Closest in time.
Scenic: A language for scenario specification and scene generation
Daniel J. Fremont, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L. Sangiovanni-Vincentelli, and Sanjit A. Seshia · 2019
Closest in time.
Explaining AI decisions using efficient methods for learning sparse boolean formulae
Susmit Jha, Tuhin Sahai, Vasumathi Raman, Alessandro Pinto, and Michael Francis · 2019
Closest in time.
Stochastic assume-guarantee contracts for cyber-physical system design
Pierluigi Nuzzo, Jiwei Li, Alberto L. Sangiovanni-Vincentelli, Yugeng Xi, and Dewei Li · 2019
Closest in time.
The seven tools of causal inference, with reflections on machine learning
Judea Pearl · 2019
Closest in time.
Introspective environment modeling
Sanjit A. Seshia · 2019
Closest in time.
Formal analysis and redesign of a neural network-based aircraft taxiing system with verifai
Daniel J. Fremont, Johnathan Chiu, Dragos D. Margineantu, Denis Osipychev, and Sanjit A. Seshia · 2020
Closest in time.
Formal scenario-based testing of autonomous vehicles: From simulation to the real world
Daniel J. Fremont, Edward Kim, Yash Vardhan Pant, Sanjit A. Seshia, Atul Acharya, Xantha Bruso, Paul Wells, Steve Lemke, Qiang Lu, and Shalin Mehta · 2020
Closest in time.