Sanjit A. Seshia

398 papers A* 42A 27B 35C 14Misc 4Journal 173Unranked 96

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Certificates in AI: Learn but Verify. Commun. ACM Clark W. Barrett, Thomas A. Henzinger, Sanjit A. Seshia
2026	J	`jnl`	Learning Contextual Runtime Monitors for Safe AI-Based Autonomy. CoRR Alejandro Luque-Cerpa, Mengyuan Wang, Emil Carlsson, Sanjit A. Seshia, Devdatt P. Dubhashi, Hazem Torfah
2026	J	`jnl`	ScenicRules: An Autonomous Driving Benchmark with Multi-Objective Specifications and Abstract Scenarios. CoRR Kevin Kai-Chun Chang, Ekin Beyazit, Alberto L. Sangiovanni-Vincentelli, Tichakorn Wongpiromsarn, Sanjit A. Seshia
2025	—	`conf`	$\mathbf{{\textsc {PyCaliper}}}$: Python-Embedded Infrastructure for RTL Verification and Specification Synthesis. CAV (3) Adwait Godbole, Brian Huffman, Fangfei Liu, Carlos V. Rozas, Sanjit A. Seshia
2025	J	`jnl`	Automata-Conditioned Cooperative Multi-Agent Reinforcement Learning. CoRR Beyazit Yalcinkaya, Marcell Vazquez-Chanlatte, Ameesh Shah, Hanna Krasowski, Sanjit A. Seshia
2025	J	`jnl`	Checking Observational Correctness of Database Systems. Proc. ACM Program. Lang. Lauren Pick, Amanda Xu, Ankush Desai, Sanjit A. Seshia, Aws Albarghouthi
2025	J	`jnl`	Clinician-Directed Large Language Model Software Generation for Therapeutic Interventions in Physical Rehabilitation. CoRR Edward Kim, Yuri Cho, Jose Eduardo E. Lima, Julie Muccini, Jenelle A. Jindal, Alison Scheid, Erik Nelson, Seong Hyun Park, Yuchen Zeng, Alton Sturgis, Caesar Li, Jackie Dai, Sun Min Kim, Yash Prakash, Liwen Sun, Isabella Hu, Hongxuan Wu, Daniel He, Wiktor Rajca, Cathra Halabi, Maarten Lansberg, Bjoern Hartmann, Sanjit A. Seshia
2025	J	`jnl`	Correction: Hypercontracts. Formal Methods Syst. Des. Inigo Incer, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2025	J	`jnl`	GRAID: Enhancing Spatial Reasoning of VLMs Through High-Fidelity Data Generation. CoRR Karim Elmaaroufi, Liheng Lai, Justin Svegliato, Yutong Bai, Sanjit A. Seshia, Matei Zaharia
2025	J	`jnl`	Hypercontracts. Formal Methods Syst. Des. Inigo Incer, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2025	J	`jnl`	Interactive Program Synthesis for Modeling Collaborative Physical Activities from Narrated Demonstrations. CoRR Edward Kim, Daniel He, Jorge Chao, Wiktor Rajca, Mohammed Amin, Nishant Malpani, Ruta Desai, Antti Oulasvirta, Bjoern Hartmann, Sanjit A. Seshia
2025	—	`ed.`	International Conference on Neuro-symbolic Systems, 28-30 May 2025, University of Pennsylvania, Philadelphia, Pennsylvania, USA. NeuS George J. Pappas, Pradeep Ravikumar, Sanjit A. Seshia
2025	—	`conf`	L*LM: Learning Automata from Demonstrations, Examples, and Natural Language. NeuS Marcell Vazquez-Chanlatte, Karim Elmaaroufi, Stefan J. Witwicki, Matei Zaharia, Sanjit A. Seshia
2025	J	`jnl`	LTL-Constrained Policy Optimization with Cycle Experience Replay. Trans. Mach. Learn. Res. Ameesh Shah, Cameron Voloshin, Chenxi Yang, Abhinav Verma, Swarat Chaudhuri, Sanjit A. Seshia
2025	J	`jnl`	Learning Affordances at Inference-Time for Vision-Language-Action Models. CoRR Ameesh Shah, William Chen, Adwait Godbole, Federico Mora, Sanjit A. Seshia, Sergey Levine
2025	—	`conf`	Learning Formal Specifications from Membership and Preference Queries. NeuS Ameesh Shah, Marcell Vazquez-Chanlatte, Sebastian Junges, Sanjit A. Seshia
2025	A	`conf`	Learning Symbolic Task Decompositions for Multi-Agent Teams. AAMAS Ameesh Shah, Niklas Lauffer, Thomas Chen, Nikhil Pitta, Sanjit A. Seshia
2025	J	`jnl`	Learning Symbolic Task Decompositions for Multi-Agent Teams. CoRR Ameesh Shah, Niklas Lauffer, Thomas Chen, Nikhil Pitta, Sanjit A. Seshia
2025	B	`conf`	Locally Pareto-Optimal Interpretations for Black-Box Machine Learning Models. ATVA Aniruddha R. Joshi, Supratik Chakraborty, S. Akshay, Shetal Shah, Hazem Torfah, Sanjit A. Seshia
2025	J	`jnl`	Locally Pareto-Optimal Interpretations for Black-Box Machine Learning Models. CoRR Aniruddha R. Joshi, Supratik Chakraborty, S. Akshay, Shetal Shah, Hazem Torfah, Sanjit A. Seshia
2025	J	`jnl`	MRTA-Sim: A Modular Simulator for Multi-Robot Allocation, Planning, and Control in Open-World Environments. CoRR Victoria Marie Tuck, Hardik Parwana, Pei-Wei Chen, Georgios Fainekos, Bardh Hoxha, Hideki Okamoto, S. Shankar Sastry, Sanjit A. Seshia
2025	—	`conf`	Mining Specifications for Predictive Safety Monitoring. ICCPS Eleonora Nesterini, Ezio Bartocci, Alessio Gambi, Dejan Nickovic, Sanjit A. Seshia, Hazem Torfah
2025	—	`conf`	Modularity in Query-Based Concept Learning. NeuS Benjamin Caulfield, Sanjit A. Seshia
2025	J	`jnl`	Pacti: Assume-Guarantee Contracts for Efficient Compositional Analysis and Design. ACM Trans. Cyber Phys. Syst. Inigo Incer, Apurva Badithela, Josefine B. Graebener, Piergiuseppe Mallozzi, Ayush Pandey, Nicolas Rouquette, Sheng-Jung Yu, Albert Benveniste, Benoît Caillaud, Richard M. Murray, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2025	B	`conf`	PolyVer: A Compositional Approach for Polyglot System Modeling and Verification. FMCAD Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward A. Lee, Sanjit A. Seshia
2025	J	`jnl`	PolyVer: A Compositional Approach for Polyglot System Modeling and Verification. CoRR Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward A. Lee, Sanjit A. Seshia
2025	—	`conf`	Provably Correct Automata Embeddings for Optimal Automata-Conditioned Reinforcement Learning. NeuS Beyazit Yalcinkaya, Niklas Lauffer, Marcell Vazquez-Chanlatte, Sanjit A. Seshia
2025	J	`jnl`	Provably Correct Automata Embeddings for Optimal Automata-Conditioned Reinforcement Learning. CoRR Beyazit Yalcinkaya, Niklas Lauffer, Marcell Vazquez-Chanlatte, Sanjit A. Seshia
2025	J	`jnl`	Quasi-Static Scheduling for Deterministic Timed Concurrent Models on Multi-Core Hardware. ACM Trans. Embed. Comput. Syst. Shaokai Lin, Erling Jellum, Mirco Theile, Tassilo Tanneberger, Binqi Sun, Chadlia Jerad, Yimo Xu, Guangyu Feng, Magnus Mæhlum, Jian-Jia Chen, Martin Schoeberl, Linh Thi Xuan Phan, Jerónimo Castrillón, Sanjit A. Seshia, Edward A. Lee
2025	—	`conf`	Querying Labeled Time Series Data with Scenario Programs. NFM Edward Kim, Devan Shanker, Varun Bharadwaj, Hongbeen Park, Jinkyu Kim, Hazem Torfah, Daniel J. Fremont, Sanjit A. Seshia
2025	J	`jnl`	Querying Labeled Time Series Data with Scenario Programs. CoRR Edward Kim, Devan Shanker, Varun Bharadwaj, Hongbeen Park, Jinkyu Kim, Hazem Torfah, Daniel J. Fremont, Sanjit A. Seshia
2025	J	`jnl`	Robust and Diverse Multi-Agent Learning via Rational Policy Gradient. CoRR Niklas Lauffer, Ameesh Shah, Micah Carroll, Sanjit A. Seshia, Stuart Russell, Michael Dennis
2025	J	`jnl`	ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems. CoRR Eric Vin, Kyle A. Miller, Inigo Incer, Sanjit A. Seshia, Daniel J. Fremont
2024	B	`conf`	Active Learning of Runtime Monitors Under Uncertainty. IFM Sebastian Junges, Sanjit A. Seshia, Hazem Torfah
2024	A*	`conf`	An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes. AAAI Amar Shah, Federico Mora, Sanjit A. Seshia
2024	A*	`conf`	Compositional Automata Embeddings for Goal-Conditioned Reinforcement Learning. NeurIPS Beyazit Yalcinkaya, Niklas Lauffer, Marcell Vazquez-Chanlatte, Sanjit A. Seshia
2024	J	`jnl`	Compositional Automata Embeddings for Goal-Conditioned Reinforcement Learning. CoRR Beyazit Yalcinkaya, Niklas Lauffer, Marcell Vazquez-Chanlatte, Sanjit A. Seshia
2024	J	`jnl`	Deep Policy Optimization with Temporal Logic Constraints. CoRR Ameesh Shah, Cameron Voloshin, Chenxi Yang, Abhinav Verma, Swarat Chaudhuri, Sanjit A. Seshia
2024	B	`conf`	Dynamic, Multi-objective Specification and Falsification of Autonomous CPS. RV Kevin Kai-Chun Chang, Kaifei Xu, Edward Kim, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2024	—	`conf`	Formal Verification Techniques for Vision-Based Autonomous Systems - A Survey. Principles of Verification (3) Sayan Mitra, Corina S. Pasareanu, Pavithra Prabhakar, Sanjit A. Seshia, Ravi Mangal, Yangge Li, Christopher Watson, Divya Gopinath, Huafeng Yu
2024	J	`jnl`	Generating Probabilistic Scenario Programs from Natural Language. CoRR Karim Elmaaroufi, Devan Shanker, Ana Cismaru, Marcell Vazquez-Chanlatte, Alberto L. Sangiovanni-Vincentelli, Matei Zaharia, Sanjit A. Seshia
2024	J	`jnl`	L CoRR Marcell Vazquez-Chanlatte, Karim Elmaaroufi, Stefan J. Witwicki, Sanjit A. Seshia
2024	—	`conf`	Lifting Micro-Update Models from RTL for Formal Security Analysis. ASPLOS (2) Adwait Godbole, Kevin Cheang, Yatin A. Manerkar, Sanjit A. Seshia
2024	J	`jnl`	PretVM: Predictable, Efficient Virtual Machine for Real-Time Concurrency. CoRR Shaokai Lin, Erling Rennemo Jellum, Mirco Theile, Tassilo Tanneberger, Binqi Sun, Chadlia Jerad, Ruomu Xu, Guangyu Feng, Christian Menard, Marten Lohstroh, Jerónimo Castrillón, Sanjit A. Seshia, Edward A. Lee
2024	J	`jnl`	Privacy Preserving Mechanisms for Coordinating Airspace Usage in Advanced Air Mobility. CoRR Chinmay Maheshwari, Maria G. Mendoza, Victoria Marie Tuck, Pan-Yang Su, Victor L. Qin, Sanjit A. Seshia, Hamsa Balakrishnan, S. Shankar Sastry
2024	—	`conf`	SMT-Based Dynamic Multi-Robot Task Allocation. NFM Victoria Marie Tuck, Pei-Wei Chen, Georgios Fainekos, Bardh Hoxha, Hideki Okamoto, S. Shankar Sastry, Sanjit A. Seshia
2024	J	`jnl`	SMT-Based Dynamic Multi-Robot Task Allocation. CoRR Victoria Marie Tuck, Pei-Wei Chen, Georgios Fainekos, Bardh Hoxha, Hideki Okamoto, S. Shankar Sastry, Sanjit A. Seshia
2024	A*	`conf`	SemPat: From Hyperproperties to Attack Patterns for Scalable Analysis of Microarchitectural Security. CCS Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia
2024	J	`jnl`	SemPat: Using Hyperproperty-based Semantic Analysis to Generate Microarchitectural Attack Patterns. CoRR Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia
2024	J	`jnl`	SimpleStrat: Diversifying Language Model Generation with Stratification. CoRR Justin Wong, Yury Orlovskiy, Michael Luo, Sanjit A. Seshia, Joseph E. Gonzalez
2024	J	`jnl`	Synthetic Programming Elicitation and Repair for Text-to-Code in Very Low-Resource Programming Languages. CoRR Federico Mora, Justin Wong, Haley Lepe, Sahil Bhatia, Karim Elmaaroufi, George Varghese, Joseph E. Gonzalez, Elizabeth Polgreen, Sanjit A. Seshia
2024	A*	`conf`	Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages. NeurIPS Federico Mora, Justin Wong, Haley Lepe, Sahil Bhatia, Karim Elmaaroufi, George Varghese, Joseph E. Gonzalez, Elizabeth Polgreen, Sanjit A. Seshia
2024	J	`jnl`	Syzygy: Dual Code-Test C to (safe) Rust Translation using LLMs and Dynamic Analysis. CoRR Manish Shetty, Naman Jain, Adwait Godbole, Sanjit A. Seshia, Koushik Sen
2024	J	`jnl`	Tenspiler: A Verified Lifting-Based Compiler for Tensor Operations. CoRR Jie Qiu, Colin Cai, Sahil Bhatia, Niranjan Hasabnis, Sanjit A. Seshia, Alvin Cheung
2024	J	`jnl`	Tenspiler: A Verified-Lifting-Based Compiler for Tensor Operations (Artifact). Dagstuhl Artifacts Ser. Jie Qiu, Colin Cai, Sahil Bhatia, Niranjan Hasabnis, Sanjit A. Seshia, Alvin Cheung
2024	A	`conf`	Tenspiler: A Verified-Lifting-Based Compiler for Tensor Operations. ECOOP Jie Qiu, Colin Cai, Sahil Bhatia, Niranjan Hasabnis, Sanjit A. Seshia, Alvin Cheung
2024	J	`jnl`	Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems. CoRR David Dalrymple, Joar Skalse, Yoshua Bengio, Stuart Russell, Max Tegmark, Sanjit A. Seshia, Steve Omohundro, Christian Szegedy, Ben Goldhaber, Nora Ammann, Alessandro Abate, Joe Halpern, Clark W. Barrett, Ding Zhao, Tan Zhi-Xuan, Jeannette M. Wing, Joshua B. Tenenbaum
2024	A*	`conf`	Verified Code Transpilation with LLMs. NeurIPS Sahil Bhatia, Jie Qiu, Niranjan Hasabnis, Sanjit A. Seshia, Alvin Cheung
2024	J	`jnl`	Verified Code Transpilation with LLMs. CoRR Sahil Bhatia, Jie Qiu, Niranjan Hasabnis, Sanjit A. Seshia, Alvin Cheung
2023	—	`conf`	3D Environment Modeling for Falsification and Beyond with Scenic 3.0. CAV (1) Eric Vin, Shun Kashiwa, Matthew Rhea, Daniel J. Fremont, Edward Kim, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2023	J	`jnl`	3D Environment Modeling for Falsification and Beyond with Scenic 3.0. CoRR Eric Vin, Shun Kashiwa, Matthew Rhea, Daniel J. Fremont, Edward Kim, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2023	J	`jnl`	A Grammar for the Representation of Unmanned Aerial Vehicles with 3D Topologies. CoRR Piergiuseppe Mallozzi, Hussein Sibai, Inigo Incer, Sanjit A. Seshia, Alberto L. Sangiovanni-Vincentelli
2023	J	`jnl`	An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes. CoRR Amar Shah, Federico Mora, Sanjit A. Seshia
2023	A	`conf`	Building Code Transpilers for Domain-Specific Languages Using Program Synthesis (Experience Paper). ECOOP Sahil Bhatia, Sumer Kohli, Sanjit A. Seshia, Alvin Cheung
2023	B	`conf`	Compositional Simulation-Based Analysis of AI-Based Autonomous Systems for Markovian Specifications. RV Beyazit Yalcinkaya, Hazem Torfah, Daniel J. Fremont, Sanjit A. Seshia
2023	J	`jnl`	Context-Aided Variable Elimination for Requirement Engineering. CoRR Inigo Incer, Albert Benveniste, Richard M. Murray, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2023	J	`jnl`	Genetic Algorithms for Searching a Matrix of Metagrammars for Synthesis. CoRR Yixuan Li, Federico Mora, Elizabeth Polgreen, Sanjit A. Seshia
2023	J	`jnl`	Learning Formal Specifications from Membership and Preference Queries. CoRR Ameesh Shah, Marcell Vazquez-Chanlatte, Sebastian Junges, Sanjit A. Seshia
2023	B	`conf`	Learning Monitor Ensembles for Operational Design Domains. RV Hazem Torfah, Aniruddha R. Joshi, Shetal Shah, S. Akshay, Supratik Chakraborty, Sanjit A. Seshia
2023	J	`jnl`	Message Chains for Distributed System Verification. Proc. ACM Program. Lang. Federico Mora, Ankush Desai, Elizabeth Polgreen, Sanjit A. Seshia
2023	B	`conf`	Modelling and Verification of Security-Oriented Resource Partitioning Schemes. FMCAD Adwait Godbole, Leiqi Ye, Yatin A. Manerkar, Sanjit A. Seshia
2023	J	`jnl`	Pacti: Scaling Assume-Guarantee Reasoning for System Analysis and Design. CoRR Inigo Incer, Apurva Badithela, Josefine Graebener, Piergiuseppe Mallozzi, Ayush Pandey, Sheng-Jung Yu, Albert Benveniste, Benoît Caillaud, Richard M. Murray, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2023	J	`jnl`	Scenic: a language for scenario specification and data generation. Mach. Learn. Daniel J. Fremont, Edward Kim, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2023	J	`jnl`	Specification-Guided Data Aggregation for Semantically Aware Imitation Learning. CoRR Ameesh Shah, Jonathan A. DeCastro, John Gideon, Beyazit Yalcinkaya, Guy Rosman, Sanjit A. Seshia
2023	—	`conf`	Symbiotic CPS Design-Space Exploration through Iterated Optimization. CPS-IoT Week Workshops Sheng-Jung Yu, Inigo Incer, Valmik Prabhu, Anwesha Chattoraj, Eric Vin, Daniel J. Fremont, Ankur Mehta, Alberto L. Sangiovanni-Vincentelli, Shankar Sastry, Sanjit A. Seshia
2023	J	`jnl`	Towards Building Verifiable CPS using Lingua Franca. ACM Trans. Embed. Comput. Syst. Shaokai Lin, Yatin A. Manerkar, Marten Lohstroh, Elizabeth Polgreen, Sheng-Jung Yu, Chadlia Jerad, Edward A. Lee, Sanjit A. Seshia
2023	J	`jnl`	Ulgen: A Runtime Assurance Framework for Programming Safe Cyber-Physical Systems. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Beyazit Yalcinkaya, Hazem Torfah, Ankush Desai, Sanjit A. Seshia
2022	J	`jnl`	A Review of Single-Source Deep Unsupervised Visual Domain Adaptation. IEEE Trans. Neural Networks Learn. Syst. Sicheng Zhao, Xiangyu Yue, Shanghang Zhang, Bo Li, Han Zhao, Bichen Wu, Ravi Krishna, Joseph E. Gonzalez, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Kurt Keutzer
2022	B	`conf`	Automated Conversion of Axiomatic to Operational Models: Theory and Practice. FMCAD Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia
2022	J	`jnl`	Automated Conversion of Axiomatic to Operational Models: Theory and Practice. CoRR Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia
2022	A*	`conf`	Cerberus: A Formal Approach to Secure and Efficient Enclave Memory Sharing. CCS Dayeol Lee, Kevin Cheang, Alexander Thomas, Catherine Lu, Pranav Gaddamadugu, Anjo Vahldiek-Oberwagner, Mona Vij, Dawn Song, Sanjit A. Seshia, Krste Asanovic
2022	J	`jnl`	Cerberus: A Formal Approach to Secure and Efficient Enclave Memory Sharing. CoRR Dayeol Lee, Kevin Cheang, Alexander Thomas, Catherine Lu, Pranav Gaddamadugu, Anjo Vahldiek-Oberwagner, Mona Vij, Dawn Song, Sanjit A. Seshia, Krste Asanovic
2022	J	`jnl`	DEC-LOS-RRT: Decentralized Path Planning for Multi-robot Systems with Line-of-sight Constrained Communication. CoRR Victoria Tuck, Yash Vardhan Pant, Sanjit A. Seshia, S. Shankar Sastry
2022	—	`conf`	Demo: Querying Labelled Data with Scenario Programs for Sim-to-Real Validation. ICCPS Edward Kim, Jay Shenoy, Sebastian Junges, Daniel J. Fremont, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2022	J	`jnl`	Emerging Technology and Policy Co-Design Considerations for the Safe and Transparent Use of Small Unmanned Aerial Systems. CoRR Ritwik Gupta, Alexander M. Bayen, Sarah Rohrschneider, Adrienne Fulk, Andrew W. Reddie, Sanjit A. Seshia, Shankar Sastry, Janet Napolitano
2022	J	`jnl`	Explorations in cyber-physical systems education. Commun. ACM Sanjit A. Seshia
2022	—	`conf`	From Interface Automata to Hypercontracts. Principles of Systems Design Inigo Incer, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2022	—	`conf`	Hypercontracts. NFM Inigo Incer, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2022	B	`conf`	Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations. FMCAD Niklas Lauffer, Beyazit Yalcinkaya, Marcell Vazquez-Chanlatte, Ameesh Shah, Sanjit A. Seshia
2022	J	`jnl`	Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations. CoRR Niklas Lauffer, Beyazit Yalcinkaya, Marcell Vazquez-Chanlatte, Ameesh Shah, Sanjit A. Seshia
2022	B	`conf`	Learning Monitorable Operational Design Domains for Assured Autonomy. ATVA Hazem Torfah, Carol Xie, Sebastian Junges, Marcell Vazquez-Chanlatte, Sanjit A. Seshia
2022	J	`jnl`	Machine learning and logic: a new frontier in artificial intelligence. Formal Methods Syst. Des. Vijay Ganesh, Sanjit A. Seshia, Somesh Jha
2022	—	`conf`	Modeling and Influencing Human Attentiveness in Autonomy-to-Human Perception Hand-offs. ITSC Yash Vardhan Pant, Balasaravanan Thoravi Kumaravel, Ameesh Shah, Erin Kraemer, Marcell Vazquez-Chanlatte, Kshitij Kulkarni, Bjoern Hartmann, Sanjit A. Seshia
2022	A*	`conf`	Programmatic Modeling and Generation of Real-Time Strategic Soccer Environments for Reinforcement Learning. AAAI Abdus Salam Azad, Edward Kim, Qiancheng Wu, Kimin Lee, Ion Stoica, Pieter Abbeel, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2022	—	`conf`	Querying Labelled Data with Scenario Programs for Sim-to-Real Validation. ICCPS Edward Kim, Jay Shenoy, Sebastian Junges, Daniel J. Fremont, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2022	B	`conf`	Satisfiability and Synthesis Modulo Oracles. VMCAI Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia
2022	J	`jnl`	Toward verified artificial intelligence. Commun. ACM Sanjit A. Seshia, Dorsa Sadigh, S. Shankar Sastry
2022	J	`jnl`	UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis. CoRR Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, Sanjit A. Seshia
2022	—	`conf`	UCLID5: Multi-modal Formal Modeling, Verification, and Synthesis. CAV (1) Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, Sanjit A. Seshia
2022	J	`jnl`	Verifying RISC-V Physical Memory Protection. CoRR Kevin Cheang, Cameron Rasmussen, Dayeol Lee, David W. Kohlbrenner, Krste Asanovic, Sanjit A. Seshia
2021	J	`jnl`	A Scenario-Based Platform for Testing Autonomous Vehicle Behavior Prediction Models in Simulation. CoRR Francis Indaheng, Edward Kim, Kesav Viswanadha, Jay Shenoy, Jinkyu Kim, Daniel J. Fremont, Sanjit A. Seshia
2021	—	`conf`	Addressing the IEEE AV Test Challenge with Scenic and VerifAI. AITest Kesav Viswanadha, Francis Indaheng, Justin Wong, Edward Kim, Ellen Kalvan, Yash Pant, Daniel J. Fremont, Sanjit A. Seshia
2021	J	`jnl`	Addressing the IEEE AV Test Challenge with Scenic and VerifAI. CoRR Kesav Viswanadha, Francis Indaheng, Justin Wong, Edward Kim, Ellen Kalvan, Yash Pant, Daniel J. Fremont, Sanjit A. Seshia
2021	J	`jnl`	Cloud-Based Quadratic Optimization With Partially Homomorphic Encryption. IEEE Trans. Autom. Control. Andreea B. Alexandru, Konstantinos Gatsis, Yasser Shoukry, Sanjit A. Seshia, Paulo Tabuada, George J. Pappas
2021	C	`conf`	Co-design of Control and Planning for Multi-rotor UAVs with Signal Temporal Logic Specifications. ACC Yash Vardhan Pant, He Yin, Murat Arcak, Sanjit A. Seshia
2021	C	`conf`	Counterexample-Guided Synthesis of Perception Models and Control. ACC Shromona Ghosh, Yash Vardhan Pant, Hadi Ravanbakhsh, Sanjit A. Seshia
2021	—	`conf`	DEC-LOS-RRT: Decentralized Path Planning for Multi-robot Systems with Line-of-sight Constrained Communication. CCTA Victoria Tuck, Yash Vardhan Pant, Sanjit A. Seshia, S. Shankar Sastry
2021	J	`jnl`	Demonstration Informed Specification Search. CoRR Marcell Vazquez-Chanlatte, Ameesh Shah, Gil Lederman, Sanjit A. Seshia
2021	—	`conf`	Enforcing Almost-Sure Reachability in POMDPs. CAV (2) Sebastian Junges, Nils Jansen, Sanjit A. Seshia
2021	—	`conf`	Entropy-Guided Control Improvisation. Robotics: Science and Systems Marcell Vazquez-Chanlatte, Sebastian Junges, Daniel J. Fremont, Sanjit A. Seshia
2021	J	`jnl`	Entropy-Guided Control Improvisation. CoRR Marcell Vazquez-Chanlatte, Sebastian Junges, Daniel J. Fremont, Sanjit A. Seshia
2021	B	`conf`	Formal Analysis of AI-Based Autonomy: From Modeling to Runtime Assurance. RV Hazem Torfah, Sebastian Junges, Daniel J. Fremont, Sanjit A. Seshia
2021	J	`jnl`	Hypercontracts. CoRR Inigo Incer, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2021	A*	`conf`	Learning Branching Heuristics for Propositional Model Counting. AAAI Pashootan Vaezipoor, Gil Lederman, Yuhuai Wu, Chris J. Maddison, Roger B. Grosse, Sanjit A. Seshia, Fahiem Bacchus
2021	A	`conf`	MedleySolver: Online SMT Algorithm Selection. SAT Nikhil Pimpalkhare, Federico Mora, Elizabeth Polgreen, Sanjit A. Seshia
2021	—	`conf`	Model Checking Finite-Horizon Markov Chains with Probabilistic Inference. CAV (2) Steven Holtzen, Sebastian Junges, Marcell Vazquez-Chanlatte, Todd D. Millstein, Sanjit A. Seshia, Guy Van den Broeck
2021	J	`jnl`	Model Checking Finite-Horizon Markov Chains with Probabilistic Inference. CoRR Steven Holtzen, Sebastian Junges, Marcell Vazquez-Chanlatte, Todd D. Millstein, Sanjit A. Seshia, Guy Van den Broeck
2021	A	`conf`	PSec: Programming Secure Distributed Systems using Enclaves. AsiaCCS Shivendra Kushwah, Ankush Desai, Pramod Subramanyan, Sanjit A. Seshia
2021	J	`jnl`	Parallel and Multi-Objective Falsification with Scenic and VerifAI. CoRR Kesav Viswanadha, Edward Kim, Francis Indaheng, Daniel J. Fremont, Sanjit A. Seshia
2021	B	`conf`	Parallel and Multi-objective Falsification with Scenic and VerifAI. RV Kesav Viswanadha, Edward Kim, Francis Indaheng, Daniel J. Fremont, Sanjit A. Seshia
2021	J	`jnl`	Querying Labelled Data with Scenario Programs for Sim-to-Real Validation. CoRR Edward Kim, Jay Shenoy, Sebastian Junges, Daniel J. Fremont, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2021	J	`jnl`	Runtime Monitoring for Markov Decision Processes. CoRR Sebastian Junges, Hazem Torfah, Sanjit A. Seshia
2021	—	`conf`	Runtime Monitors for Markov Decision Processes. CAV (2) Sebastian Junges, Hazem Torfah, Sanjit A. Seshia
2021	A*	`conf`	Safety in Autonomous Driving: Can Tools Offer Guarantees? DAC Daniel J. Fremont, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2021	—	`ch.`	Satisfiability Modulo Theories. Handbook of Satisfiability Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli
2021	J	`jnl`	Satisfiability and Synthesis Modulo Oracles. CoRR Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia
2021	J	`jnl`	Scenic4RL: Programmatic Modeling and Generation of Reinforcement Learning Environments. CoRR Abdus Salam Azad, Edward Kim, Qiancheng Wu, Kimin Lee, Ion Stoica, Pieter Abbeel, Sanjit A. Seshia
2021	B	`conf`	Synthesizing Pareto-Optimal Interpretations for Black-Box Models. FMCAD Hazem Torfah, Shetal Shah, Supratik Chakraborty, S. Akshay, Sanjit A. Seshia
2021	J	`jnl`	Synthesizing Pareto-Optimal Interpretations for Black-Box Models. CoRR Hazem Torfah, Shetal Shah, Supratik Chakraborty, S. Akshay, Sanjit A. Seshia
2020	J	`jnl`	A Customizable Dynamic Scenario Modeling and Data Generation Platform for Autonomous Driving. CoRR Jay Shenoy, Edward Kim, Xiangyu Yue, Taesung Park, Daniel J. Fremont, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2020	A*	`conf`	A Programmatic and Semantic Approach to Explaining and Debugging Neural Network Based Object Detectors. CVPR Edward Kim, Divya Gopinath, Corina S. Pasareanu, Sanjit A. Seshia
2020	J	`jnl`	A Review of Single-Source Deep Unsupervised Visual Domain Adaptation. CoRR Sicheng Zhao, Xiangyu Yue, Shanghang Zhang, Bo Li, Han Zhao, Bichen Wu, Ravi Krishna, Joseph E. Gonzalez, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Kurt Keutzer
2020	—	`conf`	Algorithmic Improvisation for Dependable Intelligent Autonomy (Invited Talk). FSTTCS Sanjit A. Seshia
2020	J	`jnl`	Co-design of Control and Planning for Multi-rotor UAVs with Signal Temporal Logic Specifications. CoRR Yash Vardhan Pant, He Yin, Murat Arcak, Sanjit A. Seshia
2020	J	`jnl`	Enforcing Almost-Sure Reachability in POMDPs. CoRR Sebastian Junges, Nils Jansen, Sanjit A. Seshia
2020	—	`conf`	Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI. CAV (1) Daniel J. Fremont, Johnathan Chiu, Dragos D. Margineantu, Denis Osipychev, Sanjit A. Seshia
2020	J	`jnl`	Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI. CoRR Daniel J. Fremont, Johnathan Chiu, Dragos D. Margineantu, Denis Osipychev, Sanjit A. Seshia
2020	—	`conf`	Formal Scenario-Based Testing of Autonomous Vehicles: From Simulation to the Real World. ITSC Daniel J. Fremont, Edward Kim, Yash Vardhan Pant, Sanjit A. Seshia, Atul Acharya, Xantha Bruso, Paul Wells, Steve Lemke, Qiang Lu, Shalin Mehta
2020	J	`jnl`	Formal Scenario-Based Testing of Autonomous Vehicles: From Simulation to the Real World. CoRR Daniel J. Fremont, Edward Kim, Yash Vardhan Pant, Sanjit A. Seshia, Atul Acharya, Xantha Bruso, Paul Wells, Steve Lemke, Qiang Lu, Shalin Mehta
2020	J	`jnl`	Gordian: Formal Reasoning-based Outlier Detection for Secure Localization. ACM Trans. Cyber Phys. Syst. Matthew Weber, Baihong Jin, Gil Lederman, Yasser Shoukry, Edward A. Lee, Sanjit A. Seshia, Alberto L. Sangiovanni-Vincentelli
2020	J	`jnl`	Gradient Descent over Metagrammars for Syntax-Guided Synthesis. CoRR Nicolas Chan, Elizabeth Polgreen, Sanjit A. Seshia
2020	—	`ed.`	HSCC '20: 23rd ACM International Conference on Hybrid Systems: Computation and Control, Sydney, New South Wales, Australia, April 21-24, 2020 HSCC Aaron D. Ames, Sanjit A. Seshia, Jyotirmoy Deshmukh
2020	J	`jnl`	Learning Branching Heuristics for Propositional Model Counting. CoRR Pashootan Vaezipoor, Gil Lederman, Yuhuai Wu, Chris J. Maddison, Roger B. Grosse, Edward A. Lee, Sanjit A. Seshia, Fahiem Bacchus
2020	A*	`conf`	Learning Heuristics for Quantified Boolean Formulas through Reinforcement Learning. ICLR Gil Lederman, Markus N. Rabe, Sanjit A. Seshia, Edward A. Lee
2020	—	`conf`	Maximum Causal Entropy Specification Inference from Demonstrations. CAV (2) Marcell Vazquez-Chanlatte, Sanjit A. Seshia
2020	B	`conf`	SOTER on ROS: A Run-Time Assurance Framework on the Robot Operating System. RV Sumukh Shivakumar, Hazem Torfah, Ankush Desai, Sanjit A. Seshia
2020	J	`jnl`	SOTER on ROS: A Run-Time Assurance Framework on the Robot Operating System. CoRR Sumukh Shivakumar, Hazem Torfah, Ankush Desai, Sanjit A. Seshia
2020	J	`jnl`	Scenic: A Language for Scenario Specification and Data Generation. CoRR Daniel J. Fremont, Edward Kim, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2020	J	`jnl`	Semantic Adversarial Deep Learning. IEEE Des. Test Sanjit A. Seshia, Somesh Jha, Tommaso Dreossi
2020	J	`jnl`	SynRG: Syntax Guided Synthesis of Invariants with Alternating Quantifiers. CoRR Elizabeth Polgreen, Sanjit A. Seshia
2020	J	`jnl`	Synthesis in Uclid5. CoRR Federico Mora, Kevin Cheang, Elizabeth Polgreen, Sanjit A. Seshia
2019	A	`conf`	A Formal Approach to Secure Speculation. CSF Kevin Cheang, Cameron Rasmussen, Sanjit A. Seshia, Pramod Subramanyan
2019	J	`jnl`	A Formal Approach to Secure Speculation. IACR Cryptol. ePrint Arch. Kevin Cheang, Cameron Rasmussen, Sanjit A. Seshia, Pramod Subramanyan
2019	J	`jnl`	A Formalization of Robustness for Deep Neural Networks. CoRR Tommaso Dreossi, Shromona Ghosh, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2019	J	`jnl`	A Model Counter's Guide to Probabilistic Systems. CoRR Marcell Vazquez-Chanlatte, Markus N. Rabe, Sanjit A. Seshia
2019	J	`jnl`	A New Simulation Metric to Determine Safe Environments and Controllers for Systems with Unknown Dynamics. CoRR Shromona Ghosh, Somil Bansal, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Claire J. Tomlin
2019	J	`jnl`	A Programmatic and Semantic Approach to Explaining and DebuggingNeural Network Based Object Detectors. CoRR Edward Kim, Divya Gopinath, Corina S. Pasareanu, Sanjit A. Seshia
2019	—	`conf`	A new simulation metric to determine safe environments and controllers for systems with unknown dynamics. HSCC Shromona Ghosh, Somil Bansal, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Claire J. Tomlin
2019	J	`jnl`	Compositional Falsification of Cyber-Physical Systems with Machine Learning Components. J. Autom. Reason. Tommaso Dreossi, Alexandre Donzé, Sanjit A. Seshia
2019	J	`jnl`	Counterexample-Guided Synthesis of Perception Models and Control. CoRR Shromona Ghosh, Hadi Ravanbakhsh, Sanjit A. Seshia
2019	—	`conf`	Flexible Computational Pipelines for Robust Abstraction-Based Control Synthesis. CAV (1) Eric S. Kim, Murat Arcak, Sanjit A. Seshia
2019	J	`jnl`	Flexible Computational Pipelines for Robust Abstraction-Based Control Synthesis. CoRR Eric S. Kim, Murat Arcak, Sanjit A. Seshia
2019	A*	`conf`	Formal Policy Learning from Demonstrations for Reachability Properties. ICRA Hadi Ravanbakhsh, Sriram Sankaranarayanan, Sanjit A. Seshia
2019	J	`jnl`	Formal Policy Learning from Demonstrations for Reachability Properties. CoRR Hadi Ravanbakhsh, Sriram Sankaranarayanan, Sanjit A. Seshia
2019	J	`jnl`	Generating Semantic Adversarial Examples with Differentiable Rendering. CoRR Lakshya Jain, Wilson Wu, Steven Chen, Uyeong Jang, Varun Chandrasekaran, Sanjit A. Seshia, Somesh Jha
2019	A	`conf`	Golden Gate: Bridging The Resource-Efficiency Gap Between ASICs and FPGA Prototypes. ICCAD Albert Magyar, David Biancolin, John Koenig, Sanjit A. Seshia, Jonathan Bachrach, Krste Asanovic
2019	B	`conf`	Introspective Environment Modeling. RV Sanjit A. Seshia
2019	J	`jnl`	Learning Task Specifications from Demonstrations via the Principle of Maximum Causal Entropy. CoRR Marcell Vazquez-Chanlatte, Sanjit A. Seshia
2019	J	`jnl`	Modularity in Query-Based Concept Learning. CoRR Benjamin Caulfield, Sanjit A. Seshia
2019	A*	`conf`	On the Utility of Learning about Humans for Human-AI Coordination. NeurIPS Micah Carroll, Rohin Shah, Mark K. Ho, Tom Griffiths, Sanjit A. Seshia, Pieter Abbeel, Anca D. Dragan
2019	J	`jnl`	On the Utility of Learning about Humans for Human-AI Coordination. CoRR Micah Carroll, Rohin Shah, Mark K. Ho, Thomas L. Griffiths, Sanjit A. Seshia, Pieter Abbeel, Anca D. Dragan
2019	C	`conf`	RTL bug localization through LTL specification mining (WIP). MEMOCODE Vighnesh Iyer, Donggyu Kim, Borivoje Nikolic, Sanjit A. Seshia
2019	J	`jnl`	Real-time Funnel Generation for Restricted Motion Planning. CoRR Hadi Ravanbakhsh, Forrest Laine, Sanjit A. Seshia
2019	A	`conf`	SOTER: A Runtime Assurance Framework for Programming Safe Robotics Systems. DSN Ankush Desai, Shromona Ghosh, Sanjit A. Seshia, Natarajan Shankar, Ashish Tiwari
2019	A*	`conf`	Scenic: a language for scenario specification and scene generation. PLDI Daniel J. Fremont, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2019	J	`jnl`	TeLEx: learning signal temporal logic from positive examples using tightness metric. Formal Methods Syst. Des. Susmit Jha, Ashish Tiwari, Sanjit A. Seshia, Tuhin Sahai, Natarajan Shankar
2019	J	`jnl`	Understanding and Extending Incremental Determinization for 2QBF. CoRR Markus N. Rabe, Leander Tentrup, Cameron Rasmussen, Sanjit A. Seshia
2019	J	`jnl`	VERIFAI: A Toolkit for the Design and Analysis of Artificial Intelligence-Based Systems. CoRR Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, Sanjit A. Seshia
2019	—	`conf`	VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems. CAV (1) Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, Sanjit A. Seshia
2018	B	`conf`	A LiDAR Point Cloud Generator: from a Virtual World to Autonomous Driving. ICMR Xiangyu Yue, Bichen Wu, Sanjit A. Seshia, Kurt Keutzer, Alberto L. Sangiovanni-Vincentelli
2018	J	`jnl`	A LiDAR Point Cloud Generator: from a Virtual World to Autonomous Driving. CoRR Xiangyu Yue, Bichen Wu, Sanjit A. Seshia, Kurt Keutzer, Alberto L. Sangiovanni-Vincentelli
2018	—	`conf`	Automatic Generation of Communication Requirements for Enforcing Multi-Agent Safety. SCAV@CPSWeek Eric S. Kim, Murat Arcak, Sanjit A. Seshia, BaekGyu Kim, Shinichi Shiraishi
2018	J	`jnl`	Cloud-based Quadratic Optimization with Partially Homomorphic Encryption. CoRR Andreea B. Alexandru, Konstantinos Gatsis, Yasser Shoukry, Sanjit A. Seshia, Paulo Tabuada, George J. Pappas
2018	J	`jnl`	Compositional programming and testing of dynamic distributed systems. Proc. ACM Program. Lang. Ankush Desai, Amar Phanishayee, Shaz Qadeer, Sanjit A. Seshia
2018	J	`jnl`	Context-Specific Validation of Data-Driven Models. CoRR Somil Bansal, Shromona Ghosh, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Claire J. Tomlin
2018	A*	`conf`	Counterexample-Guided Data Augmentation. IJCAI Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Kurt Keutzer, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2018	J	`jnl`	Counterexample-Guided Data Augmentation. CoRR Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Kurt Keutzer, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2018	—	`conf`	Cyber-Physical Systems Education: Explorations and Dreams. Principles of Modeling Sanjit A. Seshia
2018	B	`conf`	Formal Specification for Deep Neural Networks. ATVA Sanjit A. Seshia, Ankush Desai, Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, Xiangyu Yue
2018	—	`conf`	Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games. ADHS Marcell Vazquez-Chanlatte, Shromona Ghosh, Vasumathi Raman, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2018	J	`jnl`	Learning Heuristics for Automated Reasoning through Deep Reinforcement Learning. CoRR Gil Lederman, Markus N. Rabe, Sanjit A. Seshia
2018	A*	`conf`	Learning Task Specifications from Demonstrations. NeurIPS Marcell Vazquez-Chanlatte, Susmit Jha, Ashish Tiwari, Mark K. Ho, Sanjit A. Seshia
2018	—	`ch.`	Modeling for Verification. Handbook of Model Checking Sanjit A. Seshia, Natasha Sharygina, Stavros Tripakis
2018	J	`jnl`	Planning for cars that coordinate with people: leveraging effects on human actions for planning and active information gathering over human internal state. Auton. Robots Dorsa Sadigh, Nick Landolfi, Shankar S. Sastry, Sanjit A. Seshia, Anca D. Dragan
2018	—	`conf`	Programming Safe Robotics Systems: Challenges and Advances. ISoLA (2) Ankush Desai, Shaz Qadeer, Sanjit A. Seshia
2018	—	`conf`	Reactive Control Improvisation. CAV (1) Daniel J. Fremont, Sanjit A. Seshia
2018	J	`jnl`	Reactive Control Improvisation. CoRR Daniel J. Fremont, Sanjit A. Seshia
2018	J	`jnl`	SMC: Satisfiability Modulo Convex Programming. Proc. IEEE Yasser Shoukry, Pierluigi Nuzzo, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, Paulo Tabuada
2018	J	`jnl`	SMT-Based Observer Design for Cyber-Physical Systems under Sensor Attacks. ACM Trans. Cyber Phys. Syst. Yasser Shoukry, Michelle Chong, Masashi Wakaiki, Pierluigi Nuzzo, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, João Pedro Hespanha, Paulo Tabuada
2018	J	`jnl`	SOTER: Programming Safe Robotics System using Runtime Assurance. CoRR Ankush Desai, Shromona Ghosh, Sanjit A. Seshia, Natarajan Shankar, Ashish Tiwari
2018	J	`jnl`	Safe Autonomy Under Perception Uncertainty Using Chance-Constrained Temporal Logic. J. Autom. Reason. Susmit Jha, Vasumathi Raman, Dorsa Sadigh, Sanjit A. Seshia
2018	J	`jnl`	Scenic: Language-Based Scene Generation. CoRR Daniel J. Fremont, Xiangyu Yue, Tommaso Dreossi, Shromona Ghosh, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2018	—	`conf`	Semantic Adversarial Deep Learning. CAV (1) Tommaso Dreossi, Somesh Jha, Sanjit A. Seshia
2018	J	`jnl`	Semantic Adversarial Deep Learning. CoRR Tommaso Dreossi, Somesh Jha, Sanjit A. Seshia
2018	J	`jnl`	Synthesis of Obfuscation Policies to Ensure Privacy and Utility. J. Autom. Reason. Yi-Chin Wu, Vasumathi Raman, Blake C. Rawlings, Stéphane Lafortune, Sanjit A. Seshia
2018	J	`jnl`	Time Series Learning using Monotonic Logical Properties. CoRR Marcell Vazquez-Chanlatte, Shromona Ghosh, Jyotirmoy V. Deshmukh, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2018	B	`conf`	Time-Series Learning Using Monotonic Logical Properties. RV Marcell Vazquez-Chanlatte, Shromona Ghosh, Jyotirmoy V. Deshmukh, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2018	J	`jnl`	Toward an Internet of Battlefield Things: A Resilience Perspective. Computer Tarek F. Abdelzaher, Nora Ayanian, Tamer Basar, Suhas N. Diggavi, Jana Diesner, Deepak Ganesan, Ramesh Govindan, Susmit Jha, Tancrède Lepoint, Benjamin M. Marlin, Klara Nahrstedt, David M. Nicol, Raj Rajkumar, Stephen Russell, Sanjit A. Seshia, Fei Sha, Prashant J. Shenoy, Mani B. Srivastava, Gaurav S. Sukhatme, Ananthram Swami, Paulo Tabuada, Don Towsley, Nitin H. Vaidya, Venugopal V. Veeravalli
2018	C	`conf`	UCLID5: Integrating Modeling, Verification, Synthesis and Learning. MEMOCODE Sanjit A. Seshia, Pramod Subramanyan
2018	—	`conf`	Understanding and Extending Incremental Determinization for 2QBF. CAV (2) Markus N. Rabe, Leander Tentrup, Cameron Rasmussen, Sanjit A. Seshia
2018	J	`jnl`	Unsupervised Domain Adaptation: from Simulation Engine to the RealWorld. CoRR Sicheng Zhao, Bichen Wu, Joseph Gonzalez, Sanjit A. Seshia, Kurt Keutzer
2018	A	`conf`	Will Distributed Computing Revolutionize Peace? The Emergence of Battlefield IoT. ICDCS Tarek F. Abdelzaher, Nora Ayanian, Tamer Basar, Suhas N. Diggavi, Jana Diesner, Deepak Ganesan, Ramesh Govindan, Susmit Jha, Tancrède Lepoint, Benjamin M. Marlin, Klara Nahrstedt, David M. Nicol, Raj Rajkumar, Stephen Russell, Sanjit A. Seshia, Fei Sha, Prashant J. Shenoy, Mani B. Srivastava, Gaurav S. Sukhatme, Ananthram Swami, Paulo Tabuada, Don Towsley, Nitin H. Vaidya, Venugopal V. Veeravalli
2017	J	`jnl`	2016 IEEE Education Society Awards, 2016 Frontiers in Education Conference Awards, and Selected IEEE Awards. IEEE Trans. Educ. Edwin C. Jones, Kathleen E. Wage, Sanjit A. Seshia, Susan M. Lord, Michael E. Auer, Lance C. Pérez, Katherine Shu-Min Li, S. L. Krishna Priya, Sasha Nikolic, Francisco Arcega, Richard A. Layton, Matthew W. Ohland, Kayode Peter Ayodele, Isaac A. Inyang, Lawrence O. Kehinde, Jana Reisslein, Amy M. Johnson, Martin Reisslein, James L. Huff, Joachim Walther, Brent K. Jesiek, Carla B. Zoltowski, William C. Oakes, Natasha Nesiba, Enrico Pontelli, Timothy Staley, Melany M. Ciampi, John Heywood, Diane T. Rover, Raman M. Unnikrishnan, Agnieszka Miguel
2017	A*	`conf`	A Formal Foundation for Secure Remote Execution of Enclaves. CCS Pramod Subramanyan, Rohit Sinha, Ilia A. Lebedev, Srinivas Devadas, Sanjit A. Seshia
2017	J	`jnl`	A Formal Foundation for Secure Remote Execution of Enclaves. IACR Cryptol. ePrint Arch. Pramod Subramanyan, Rohit Sinha, Ilia A. Lebedev, Srinivas Devadas, Sanjit A. Seshia
2017	—	`conf`	A Small Gain Theorem for Parametric Assume-Guarantee Contracts. HSCC Eric S. Kim, Murat Arcak, Sanjit A. Seshia
2017	—	`conf`	A compiler and verifier for page access oblivious computation. ESEC/SIGSOFT FSE Rohit Sinha, Sriram K. Rajamani, Sanjit A. Seshia
2017	J	`jnl`	A theory of formal synthesis via inductive learning. Acta Informatica Susmit Jha, Sanjit A. Seshia
2017	—	`conf`	Active Preference-Based Learning of Reward Functions. Robotics: Science and Systems Dorsa Sadigh, Anca D. Dragan, Shankar Sastry, Sanjit A. Seshia
2017	B	`conf`	Combining Model Checking and Runtime Verification for Safe Robotics. RV Ankush Desai, Tommaso Dreossi, Sanjit A. Seshia
2017	—	`conf`	Compositional Falsification of Cyber-Physical Systems with Machine Learning Components. NFM Tommaso Dreossi, Alexandre Donzé, Sanjit A. Seshia
2017	J	`jnl`	Compositional Falsification of Cyber-Physical Systems with Machine Learning Components. CoRR Tommaso Dreossi, Alexandre Donzé, Sanjit A. Seshia
2017	J	`jnl`	Control Improvisation. CoRR Daniel J. Fremont, Alexandre Donzé, Sanjit A. Seshia
2017	—	`conf`	DRONA: a framework for safe distributed mobile robotics. ICCPS Ankush Desai, Indranil Saha, Jianqiao Yang, Shaz Qadeer, Sanjit A. Seshia
2017	J	`jnl`	Design Automation of Cyber-Physical Systems: Challenges, Advances, and Opportunities. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Sanjit A. Seshia, Shiyan Hu, Wenchao Li, Qi Zhu
2017	—	`conf`	Dynamic contracts for distributed temporal logic control of traffic networks. CDC Eric S. Kim, Sadra Sadraddini, Calin Belta, Murat Arcak, Sanjit A. Seshia
2017	—	`conf`	Linear temporal logic motion planning for teams of underactuated robots using satisfiability modulo convex programming. CDC Yasser Shoukry, Pierluigi Nuzzo, Ayca Balkan, Indranil Saha, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, Paulo Tabuada
2017	—	`conf`	Logical Clustering and Learning for Time-Series Data. CAV (1) Marcell Vazquez-Chanlatte, Jyotirmoy V. Deshmukh, Xiaoqing Jin, Sanjit A. Seshia
2017	J	`jnl`	Machine Learning and Formal Method (Dagstuhl Seminar 17351). Dagstuhl Reports Sanjit A. Seshia, Xiaojin (Jerry) Zhu, Andreas Krause, Susmit Jha
2017	A*	`conf`	Maximum Model Counting. AAAI Daniel J. Fremont, Markus N. Rabe, Sanjit A. Seshia
2017	J	`jnl`	Model Predictive Control for Signal Temporal Logic Specification. CoRR Vasumathi Raman, Alexandre Donzé, Mehdi Maasoumy, Richard M. Murray, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2017	J	`jnl`	Program synthesis for interactive-security systems. Formal Methods Syst. Des. William R. Harris, Somesh Jha, Thomas W. Reps, Sanjit A. Seshia
2017	J	`jnl`	Robust online monitoring of signal temporal logic. Formal Methods Syst. Des. Jyotirmoy V. Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, Sanjit A. Seshia
2017	—	`conf`	SMC: Satisfiability Modulo Convex Optimization. HSCC Yasser Shoukry, Pierluigi Nuzzo, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, Paulo Tabuada
2017	J	`jnl`	Secure State Estimation for Cyber-Physical Systems Under Sensor Attacks: A Satisfiability Modulo Theory Approach. IEEE Trans. Autom. Control. Yasser Shoukry, Pierluigi Nuzzo, Alberto Puggelli, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Paulo Tabuada
2017	J	`jnl`	Specification Inference from Demonstrations. CoRR Marcell Vazquez-Chanlatte, Susmit Jha, Ashish Tiwari, Sanjit A. Seshia
2017	C	`conf`	Stochastic predictive freeway ramp metering from Signal Temporal Logic specifications. ACC Negar Mehr, Dorsa Sadigh, Roberto Horowitz, S. Shankar Sastry, Sanjit A. Seshia
2017	J	`jnl`	Symbolic control design for monotone systems with directed specifications. Autom. Eric S. Kim, Murat Arcak, Sanjit A. Seshia
2017	J	`jnl`	Systematic Testing of Convolutional Neural Networks for Autonomous Driving. CoRR Tommaso Dreossi, Shromona Ghosh, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2017	B	`conf`	TeLEx: Passive STL Learning Using Only Positive Examples. RV Susmit Jha, Ashish Tiwari, Sanjit A. Seshia, Tuhin Sahai, Natarajan Shankar
2017	J	`jnl`	Tunable Reactive Synthesis for Lipschitz-Bounded Systems with Temporal Logic Specifications. CoRR Marcell Vazquez-Chanlatte, Shromona Ghosh, Vasumathi Raman, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2016	A*	`conf`	A design and verification methodology for secure isolated regions. PLDI Rohit Sinha, Manuel Costa, Akash Lal, Nuno P. Lopes, Sriram K. Rajamani, Sanjit A. Seshia, Kapil Vaswani
2016	C	`conf`	Assume-guarantee contracts and controller synthesis for vehicular traffic networks. ACC Eric S. Kim, Murat Arcak, Sanjit A. Seshia
2016	B	`conf`	Combining requirement mining, software model checking and simulation-based verification for industrial automotive systems. FMCAD Tomoya Yamaguchi, Tomoyuki Kaga, Alexandre Donzé, Sanjit A. Seshia
2016	—	`conf`	Constrained Sampling and Counting: Universal Hashing Meets SAT Solving. AAAI Workshop: Beyond NP Kuldeep S. Meel, Moshe Y. Vardi, Supratik Chakraborty, Daniel J. Fremont, Sanjit A. Seshia, Dror Fried, Alexander Ivrii, Sharad Malik
2016	—	`conf`	Control Improvisation with Probabilistic Temporal Specifications. IoTDI Ilge Akkaya, Daniel J. Fremont, Rafael Valle, Alexandre Donzé, Edward A. Lee, Sanjit A. Seshia
2016	—	`conf`	Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications. HSCC Shromona Ghosh, Dorsa Sadigh, Pierluigi Nuzzo, Vasumathi Raman, Alexandre Donzé, Alberto L. Sangiovanni-Vincentelli, S. Shankar Sastry, Sanjit A. Seshia
2016	J	`jnl`	Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications. CoRR Shromona Ghosh, Dorsa Sadigh, Pierluigi Nuzzo, Vasumathi Raman, Alexandre Donzé, Alberto L. Sangiovanni-Vincentelli, S. Shankar Sastry, Sanjit A. Seshia
2016	—	`conf`	Directed Specifications and Assumption Mining for Monotone Dynamical Systems. HSCC Eric S. Kim, Murat Arcak, Sanjit A. Seshia
2016	—	`conf`	Implan: Scalable Incremental Motion Planning for Multi-Robot Systems. ICCPS Indranil Saha, Rattanachai Ramaithitima, Vijay Kumar, George J. Pappas, Sanjit A. Seshia
2016	A	`conf`	Incremental Determinization. SAT Markus N. Rabe, Sanjit A. Seshia
2016	A	`conf`	Information gathering actions over human internal state. IROS Dorsa Sadigh, S. Shankar Sastry, Sanjit A. Seshia, Anca D. Dragan
2016	J	`jnl`	Learning Auditable Features from Signals Using Unsupervised Temporal Projection. CoRR Marcell V.-Chanlatte, Jyotirmoy V. Deshmukh, Xiaoqing Jin, Sanjit A. Seshia
2016	—	`conf`	Learning and Visualizing Music Specifications Using Pattern Graphs. ISMIR Rafael Valle, Daniel J. Fremont, Ilge Akkaya, Alexandre Donzé, Adrian Freed, Sanjit A. Seshia
2016	—	`conf`	Obfuscator Synthesis for Privacy and Utility. NFM Yi-Chin Wu, Vasumathi Raman, Stéphane Lafortune, Sanjit A. Seshia
2016	A	`conf`	On the Hardness of SAT with Community Structure. SAT Nathan Mull, Daniel J. Fremont, Sanjit A. Seshia
2016	J	`jnl`	On the Hardness of SAT with Community Structure. CoRR Nathan Mull, Daniel J. Fremont, Sanjit A. Seshia
2016	B	`conf`	On ∃ ∀ ∃! solving: A case study on automated synthesis of magic card tricks. FMCAD Susmit Jha, Vasumathi Raman, Sanjit A. Seshia
2016	—	`conf`	Planning for Autonomous Cars that Leverage Effects on Human Actions. Robotics: Science and Systems Dorsa Sadigh, Shankar Sastry, Sanjit A. Seshia, Anca D. Dragan
2016	—	`conf`	Privacy-aware quadratic optimization using partially homomorphic encryption. CDC Yasser Shoukry, Konstantinos Gatsis, Amr Al-Anwar, George J. Pappas, Sanjit A. Seshia, Mani B. Srivastava, Paulo Tabuada
2016	—	`conf`	SMT-Based Observer Design for Cyber-Physical Systems under Sensor Attacks. ICCPS Yasser Shoukry, Michelle Chong, Masashi Wakaiki, Pierluigi Nuzzo, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, João Pedro Hespanha, Paulo Tabuada
2016	—	`conf`	Scalable lazy SMT-based motion planning. CDC Yasser Shoukry, Pierluigi Nuzzo, Indranil Saha, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, Paulo Tabuada
2016	J	`jnl`	Specification Mining for Machine Improvisation with Formal Specifications. Comput. Entertain. Rafael Valle, Alexandre Donzé, Daniel J. Fremont, Ilge Akkaya, Sanjit A. Seshia, Adrian Freed, David Wessel
2016	J	`jnl`	Towards Verified Artificial Intelligence. CoRR Sanjit A. Seshia, Dorsa Sadigh
2016	—	`conf`	Towards trustworthy automation: User interfaces that convey internal and external awareness. ITSC Tara Rezvani, Katherine Rose Driggs-Campbell, Dorsa Sadigh, S. Shankar Sastry, Sanjit A. Seshia, Ruzena Bajcsy
2016	—	`ed.`	Verified Software: Theories, Tools, and Experiments - 7th International Conference, VSTTE 2015, San Francisco, CA, USA, July 18-19, 2015. Revised Selected Papers VSTTE Arie Gurfinkel, Sanjit A. Seshia
2016	—	`conf`	ddNF: An Efficient Data Structure for Header Spaces. Haifa Verification Conference Nikolaj S. Bjørner, Garvit Juniwal, Ratul Mahajan, Sanjit A. Seshia, George Varghese
2015	J	`jnl`	A Satisfiability Modulo Theory Approach to Secure State Reconstruction in Differentially Flat Systems Under Sensor Attacks. CoRR Yasser Shoukry, Pierluigi Nuzzo, Nicola Bezzo, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Paulo Tabuada
2015	J	`jnl`	A Theory of Formal Synthesis via Inductive Learning. CoRR Susmit Jha, Sanjit A. Seshia
2015	—	`conf`	Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems. CAV (2) Ankush Desai, Sanjit A. Seshia, Shaz Qadeer, David Broman, John C. Eidson
2015	C	`conf`	Automotive systems requirement mining using breach. ACC Alexandre Donzé, Xiaoqing Jin, Jyotirmoy V. Deshmukh, Sanjit A. Seshia
2015	B	`conf`	Clustering-Based Active Learning for CPSGrader. L@S Garvit Juniwal, Sakshi Jain, Alexandre Donzé, Sanjit A. Seshia
2015	J	`jnl`	Combining Induction, Deduction, and Structure for Verification and Synthesis. Proc. IEEE Sanjit A. Seshia
2015	—	`conf`	Compositional controller synthesis for vehicular traffic networks. CDC Eric S. Kim, Murat Arcak, Sanjit A. Seshia
2015	J	`jnl`	Constrained Sampling and Counting: Universal Hashing Meets SAT Solving. CoRR Kuldeep S. Meel, Moshe Y. Vardi, Supratik Chakraborty, Daniel J. Fremont, Sanjit A. Seshia, Dror Fried, Alexander Ivrii, Sharad Malik
2015	J	`jnl`	Control Improvisation with Probabilistic Temporal Specifications. CoRR Ilge Akkaya, Daniel J. Fremont, Rafael Valle, Alexandre Donzé, Edward A. Lee, Sanjit A. Seshia
2015	—	`conf`	Control Improvisation. FSTTCS Daniel J. Fremont, Alexandre Donzé, Sanjit A. Seshia, David Wessel
2015	A*	`conf`	Formal methods for semi-autonomous driving. DAC Sanjit A. Seshia, Dorsa Sadigh, S. Shankar Sastry
2015	J	`jnl`	Mining Requirements From Closed-Loop Control Models. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Xiaoqing Jin, Alexandre Donzé, Jyotirmoy V. Deshmukh, Sanjit A. Seshia
2015	A*	`conf`	Moat: Verifying Confidentiality of Enclave Programs. CCS Rohit Sinha, Sriram K. Rajamani, Sanjit A. Seshia, Kapil Vaswani
2015	A	`conf`	On Parallel Scalable Uniform SAT Witness Generation. TACAS Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, Moshe Y. Vardi
2015	J	`jnl`	On Systematic Testing for Execution-Time Analysis. CoRR Daniel Bundala, Sanjit A. Seshia
2015	—	`conf`	Reactive synthesis from signal temporal logic specifications. HSCC Vasumathi Raman, Alexandre Donzé, Dorsa Sadigh, Richard M. Murray, Sanjit A. Seshia
2015	B	`conf`	Robust Online Monitoring of Signal Temporal Logic. RV Jyotirmoy V. Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, Sanjit A. Seshia
2015	J	`jnl`	Robust Online Monitoring of Signal Temporal Logic. CoRR Jyotirmoy V. Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, Sanjit A. Seshia
2015	—	`conf`	Secure state reconstruction in differentially flat systems under sensor attacks using satisfiability modulo theory solving. CDC Yasser Shoukry, Pierluigi Nuzzo, Nicola Bezzo, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Paulo Tabuada
2015	C	`conf`	Sound and complete state estimation for linear dynamical systems under sensor attacks using Satisfiability Modulo Theory solving. ACC Yasser Shoukry, Alberto Puggelli, Pierluigi Nuzzo, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Paulo Tabuada
2015	—	`ch.`	Syntax-Guided Synthesis. Dependable Software Systems Engineering Rajeev Alur, Rastislav Bodík, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Abhishek Udupa
2015	—	`conf`	Systematic testing of asynchronous reactive systems. ESEC/SIGSOFT FSE Ankush Desai, Shaz Qadeer, Sanjit A. Seshia
2015	J	`jnl`	What's Decidable about Syntax-Guided Synthesis? CoRR Benjamin Caulfield, Markus N. Rabe, Sanjit A. Seshia, Stavros Tripakis
2014	J	`jnl`	A Contract-Based Methodology for Aircraft Electric Power System Design. IEEE Access Pierluigi Nuzzo, Huan Xu, Necmiye Ozay, John B. Finn, Alberto L. Sangiovanni-Vincentelli, Richard M. Murray, Alexandre Donzé, Sanjit A. Seshia
2014	J	`jnl`	A Learning Based Approach to Control Synthesis of Markov Decision Processes for Linear Temporal Logic Specifications. CoRR Dorsa Sadigh, Eric S. Kim, Samuel Coogan, S. Shankar Sastry, Sanjit A. Seshia
2014	—	`conf`	A learning based approach to control synthesis of Markov decision processes for linear temporal logic specifications. CDC Dorsa Sadigh, Eric S. Kim, Samuel Coogan, S. Shankar Sastry, Sanjit A. Seshia
2014	—	`conf`	Are There Good Mistakes? A Theoretical Analysis of CEGIS. SYNT Susmit Jha, Sanjit A. Seshia
2014	A	`conf`	Automated composition of motion primitives for multi-robot systems from safe LTL specifications. IROS Indranil Saha, Rattanachai Ramaithitima, Vijay Kumar, George J. Pappas, Sanjit A. Seshia
2014	Misc	`conf`	CPSGrader: Synthesizing temporal logic testers for auto-grading an embedded systems laboratory. EMSOFT Garvit Juniwal, Alexandre Donzé, Jeff C. Jensen, Sanjit A. Seshia
2014	J	`jnl`	Compositional Performance Verification of Network-on-Chip Designs. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Daniel E. Holcomb, Sanjit A. Seshia
2014	J	`jnl`	Control Improvisation. CoRR Daniel J. Fremont, Alexandre Donzé, Sanjit A. Seshia, David Wessel
2014	—	`conf`	Data-Driven Probabilistic Modeling and Verification of Human Driver Behavior. AAAI Spring Symposia Dorsa Sadigh, Katherine Rose Driggs-Campbell, Alberto Puggelli, Wenchao Li, Victor Shia, Ruzena Bajcsy, Alberto L. Sangiovanni-Vincentelli, S. Shankar Sastry, Sanjit A. Seshia
2014	J	`jnl`	Decision Procedures and Abstract Interpretation (Dagstuhl Seminar 14351). Dagstuhl Reports Daniel Kroening, Thomas W. Reps, Sanjit A. Seshia, Aditya V. Thakur
2014	—	`conf`	Distributed control of a swarm of buildings connected to a smart grid: demo abstract. BuildSys Baris Aksanli, Alper Sinan Akyurek, Madhur Behl, Meghan Clark, Alexandre Donzé, Prabal Dutta, Patrick Lazik, Mehdi Maasoumy, Rahul Mangharam, Truong X. Nghiem, Vasumathi Raman, Anthony Rowe, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Tajana Simunic Rosing, Jagannathan Venkatesh
2014	A*	`conf`	Distribution-Aware Sampling and Weighted Model Counting for SAT. AAAI Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, Moshe Y. Vardi
2014	J	`jnl`	Distribution-Aware Sampling and Weighted Model Counting for SAT. CoRR Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, Moshe Y. Vardi
2014	—	`conf`	Formal Modeling and Verification of CloudProxy. VSTTE Wei Yang Tan, Rohit Sinha, John L. Manferdelli, Sanjit A. Seshia
2014	—	`conf`	Game theoretic secure localization in wireless sensor networks. IOT Susmit Jha, Stavros Tripakis, Sanjit A. Seshia, Krishnendu Chatterjee
2014	—	`conf`	Machine Improvisation with Formal Specifications. ICMC Alexandre Donzé, Rafael Valle, Ilge Akkaya, Sophie Libkind, Sanjit A. Seshia, David Wessel
2014	—	`conf`	Model predictive control with signal temporal logic specifications. CDC Vasumathi Raman, Alexandre Donzé, Mehdi Maasoumy, Richard M. Murray, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2014	J	`jnl`	Reverse Engineering Digital Circuits Using Structural and Functional Analyses. IEEE Trans. Emerg. Top. Comput. Pramod Subramanyan, Nestan Tsiskaridze, Wenchao Li, Adrià Gascón, Wei Yang Tan, Ashish Tiwari, Natarajan Shankar, Sanjit A. Seshia, Sharad Malik
2014	Misc	`conf`	Robust strategy synthesis for probabilistic systems applied to risk-limiting renewable-energy pricing. EMSOFT Alberto Puggelli, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2014	—	`conf`	Safety envelope for security. HiCoNS Ashish Tiwari, Bruno Dutertre, Dejan Jovanovic, Thomas de Candia, Patrick Lincoln, John M. Rushby, Dorsa Sadigh, Sanjit A. Seshia
2014	J	`jnl`	Secure State Estimation Under Sensor Attacks: A Satisfiability Modulo Theory Approach. CoRR Yasser Shoukry, Pierluigi Nuzzo, Alberto Puggelli, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Paulo Tabuada
2014	—	`conf`	Speeding Up SMT-Based Quantitative Program Analysis. SMT Daniel J. Fremont, Sanjit A. Seshia
2014	J	`jnl`	Speeding Up SMT-Based Quantitative Program Analysis. CoRR Daniel J. Fremont, Sanjit A. Seshia
2014	A	`conf`	Synthesis for Human-in-the-Loop Control Systems. TACAS Wenchao Li, Dorsa Sadigh, S. Shankar Sastry, Sanjit A. Seshia
2014	B	`conf`	Synthesis with Identifiers. VMCAI Rüdiger Ehlers, Sanjit A. Seshia, Hadas Kress-Gazit
2014	J	`jnl`	The Swarm at the Edge of the Cloud. IEEE Des. Test Edward A. Lee, Björn Hartmann, John Kubiatowicz, Tajana Simunic Rosing, John Wawrzynek, David Wessel, Jan M. Rabaey, Kris Pister, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, David T. Blaauw, Prabal Dutta, Kevin Fu, Carlos Guestrin, Ben Taskar, Roozbeh Jafari, Douglas L. Jones, Vijay Kumar, Rahul Mangharam, George J. Pappas, Richard M. Murray, Anthony Rowe
2014	—	`conf`	User interface design and verification for semi-autonomous driving. HiCoNS Dorsa Sadigh, Katherine Rose Driggs-Campbell, Ruzena Bajcsy, S. Shankar Sastry, Sanjit A. Seshia
2013	—	`conf`	Mining requirements from closed-loop control models. HSCC Xiaoqing Jin, Alexandre Donzé, Jyotirmoy V. Deshmukh, Sanjit A. Seshia
2013	A*	`conf`	Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. CAV Alberto Puggelli, Wenchao Li, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2013	J	`jnl`	Robust Subspace System Identification via Weighted Nuclear Norm Optimization. CoRR Dorsa Sadigh, Henrik Ohlsson, S. Shankar Sastry, Sanjit A. Seshia
2013	J	`jnl`	SWATI: Synthesizing Wordlengths Automatically Using Testing and Induction CoRR Susmit Jha, Sanjit A. Seshia
2013	C	`conf`	Symbolic software model validation. MEMOCODE Cynthia Sturton, Rohit Sinha, Thurston H. Y. Dang, Sakshi Jain, Michael McCoyd, Wei Yang Tan, Petros Maniatis, Sanjit A. Seshia, David A. Wagner
2013	B	`conf`	Syntax-guided synthesis. FMCAD Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Abhishek Udupa
2013	C	`conf`	Synthesis of Implementable Control Strategies for Lazy Linear Hybrid Automata. FedCSIS Luigi Di Guglielmo, Sanjit A. Seshia, Tiziano Villa
2013	Misc	`conf`	Verifying High-Confidence Interactive Systems: Electronic Voting and Beyond. ICDCN Sanjit A. Seshia
2013	—	`conf`	WordRev: Finding word-level structures in a sea of bit-level gates. HOST Wenchao Li, Adrià Gascón, Pramod Subramanyan, Wei Yang Tan, Ashish Tiwari, Sharad Malik, Natarajan Shankar, Sanjit A. Seshia
2012	—	`conf`	Automating exercise generation: a step towards meeting the MOOC challenge for embedded systems. WESE Dorsa Sadigh, Sanjit A. Seshia, Mona Gupta
2012	C	`conf`	Compositional performance verification of NoC designs. MEMOCODE Daniel E. Holcomb, Alexander Gotmanov, Michael Kishinevsky, Sanjit A. Seshia
2012	A*	`ed.`	Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings CAV P. Madhusudan, Sanjit A. Seshia
2012	A*	`conf`	CrowdMine: towards crowdsourced human-assisted verification. DAC Wenchao Li, Sanjit A. Seshia, Somesh Jha
2012	J	`jnl`	Distributed Real-Time Software for Cyber-Physical Systems. Proc. IEEE John C. Eidson, Edward A. Lee, Slobodan Matic, Sanjit A. Seshia, Jia Zou
2012	J	`jnl`	Quantitative Analysis of Systems Using Game-Theoretic Learning. ACM Trans. Embed. Comput. Syst. Sanjit A. Seshia, Alexander Rakhlin
2012	—	`conf`	Reverse engineering circuits using behavioral pattern mining. HOST Wenchao Li, Zach Wasson, Sanjit A. Seshia
2012	J	`jnl`	Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis CoRR Sanjit A. Seshia
2012	A*	`conf`	Sciduction: combining induction, deduction, and structure for verification and synthesis. DAC Sanjit A. Seshia
2012	B	`conf`	Sparse Coding for Specification Mining and Error Localization. RV Wenchao Li, Sanjit A. Seshia
2012	—	`conf`	Teaching embedded systems the Berkeley way. WESE Edward A. Lee, Sanjit A. Seshia, Jeff C. Jensen
2012	B	`conf`	Verification with small and short worlds. FMCAD Rohit Sinha, Cynthia Sturton, Petros Maniatis, Sanjit A. Seshia, David A. Wagner
2011	A*	`conf`	Abstraction-based performance verification of NoCs. DAC Daniel E. Holcomb, Bryan A. Brady, Sanjit A. Seshia
2011	C	`conf`	An introductory capstone design course on embedded systems. ISCAS Jeff C. Jensen, Edward A. Lee, Sanjit A. Seshia
2011	A	`conf`	Counterexample-guided SMT-driven optimal buffer sizing. DATE Bryan A. Brady, Daniel E. Holcomb, Sanjit A. Seshia
2011	A	`conf`	GameTime: A Toolkit for Timing Analysis of Software. TACAS Sanjit A. Seshia, Jonathan Kotker
2011	B	`conf`	Learning conditional abstractions. FMCAD Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia
2011	C	`conf`	Mining assumptions for synthesis. MEMOCODE Wenchao Li, Lili Dworkin, Sanjit A. Seshia
2011	Misc	`conf`	Synthesis of optimal switching logic for hybrid systems. EMSOFT Susmit Jha, Sanjit A. Seshia, Ashish Tiwari
2011	—	`conf`	Synthesis with Clairvoyance. Haifa Verification Conference Orna Kupferman, Dorsa Sadigh, Sanjit A. Seshia
2011	J	`jnl`	Synthesizing Switching Logic to Minimize Long-Run Cost CoRR Susmit Jha, Sanjit A. Seshia, Ashish Tiwari
2011	B	`conf`	Timing analysis of interrupt-driven programs under context bounds. FMCAD Jonathan Kotker, Dorsa Sadigh, Sanjit A. Seshia
2010	C	`conf`	ATLAS: Automatic Term-level abstraction of RTL designs. MEMOCODE Bryan A. Brady, Randal E. Bryant, Sanjit A. Seshia, John W. O'Leary
2010	—	`conf`	An introductory textbook on cyber-physical systems. WESE Edward A. Lee, Sanjit A. Seshia
2010	A	`conf`	Automating Security Mediation Placement. ESOP Dave King, Susmit Jha, Divya Muthukumaran, Trent Jaeger, Somesh Jha, Sanjit A. Seshia
2010	B	`conf`	CalCS: SMT solving for non-linear convex constraints. FMCAD Pierluigi Nuzzo, Alberto Puggelli, Sanjit A. Seshia, Alberto L. Sangiovanni-Vincentelli
2010	—	`conf`	Oracle-guided component-based program synthesis. ICSE (1) Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari
2010	A*	`conf`	Post-silicon validation opportunities, challenges and recent advances. DAC Subhasish Mitra, Sanjit A. Seshia, Nicola Nicolici
2010	—	`conf`	Quantitative Analysis of Software: Challenges and Recent Advances. FACS Sanjit A. Seshia
2010	A*	`conf`	Scalable specification mining for verification and diagnosis. DAC Wenchao Li, Alessandro Forin, Sanjit A. Seshia
2010	—	`conf`	Synthesizing switching logic for safety and dwell-time requirements. ICCPS Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari
2009	J	`jnl`	An abstraction-based decision procedure for bit-vector arithmetic. Int. J. Softw. Tools Technol. Transf. Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady
2009	A*	`conf`	Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic. CAV Susmit Jha, Rhishikesh Limaye, Sanjit A. Seshia
2009	A	`conf`	Design as you see FIT: System-level soft error analysis of sequential circuits. DATE Daniel E. Holcomb, Wenchao Li, Sanjit A. Seshia
2009	—	`conf`	Localizing transient faults using dynamic bayesian networks. HLDVT Susmit Jha, Wenchao Li, Sanjit A. Seshia
2009	J	`jnl`	On the Computational Complexity of Satisfiability Solving for String Theories CoRR Susmit Jha, Sanjit A. Seshia, Rhishikesh Limaye
2009	A*	`conf`	On voting machine design for verification and testability. CCS Cynthia Sturton, Susmit Jha, Sanjit A. Seshia, David A. Wagner
2009	A	`conf`	Optimizations of an application-level protocol for enhanced dependability in FlexRay. DATE Wenchao Li, Marco Di Natale, Wei Zheng, Paolo Giusto, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia
2009	—	`ch.`	Satisfiability Modulo Theories. Handbook of Satisfiability Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli
2009	—	`conf`	The Case for Timing-Centric Distributed Software Invited Paper. ICDCS Workshops Edward A. Lee, Slobodan Matic, Sanjit A. Seshia, Jia Zou
2008	B	`conf`	A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance. FMCAD Orna Kupferman, Wenchao Li, Sanjit A. Seshia
2008	—	`conf`	Effective blame for information-flow violations. SIGSOFT FSE Dave King, Trent Jaeger, Somesh Jha, Sanjit A. Seshia
2008	A	`conf`	Game-theoretic timing analysis. ICCAD Sanjit A. Seshia, Alexander Rakhlin
2007	A	`conf`	An Application ofWeb-Service Interfaces. ICWS Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger, Sanjit A. Seshia
2007	—	`conf`	Autonomic Reactive Systems via Online Learning. ICAC Sanjit A. Seshia
2007	A	`conf`	Deciding Bit-Vector Arithmetic with Abstraction. TACAS Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady
2007	A	`conf`	Formal verification at higher levels of abstraction. ICCAD Daniel Kroening, Sanjit A. Seshia
2007	A	`conf`	Interactive presentation: Automatic model generation for black box real-time systems. DATE Thomas Huining Feng, Lynn Wang, Wei Zheng, Sri Kanajan, Sanjit A. Seshia
2007	J	`jnl`	On Solving Boolean Combinations of UTVPI Constraints. J. Satisf. Boolean Model. Comput. Sanjit A. Seshia, K. Subramani, Randal E. Bryant
2007	A*	`conf`	Sketching stencils. PLDI Armando Solar-Lezama, Gilad Arnold, Liviu Tancau, Rastislav Bodík, Vijay A. Saraswat, Sanjit A. Seshia
2007	—	`conf`	Symbolic Reachability Analysis of Lazy Linear Hybrid Automata. FORMATS Susmit Jha, Bryan A. Brady, Sanjit A. Seshia
2007	A	`conf`	Verification-guided soft error resilience. DATE Sanjit A. Seshia, Wenchao Li, Subhasish Mitra
2006	A*	`conf`	Combinatorial sketching for finite programs. ASPLOS Armando Solar-Lezama, Liviu Tancau, Rastislav Bodík, Sanjit A. Seshia, Vijay A. Saraswat
2005	A*	`conf`	Automatic discovery of API-level exploits. ICSE Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, Randal E. Bryant
2005	J	`jnl`	Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds CoRR Sanjit A. Seshia, Randal E. Bryant
2005	J	`jnl`	Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. Log. Methods Comput. Sci. Sanjit A. Seshia, Randal E. Bryant
2005	A	`conf`	Decision Procedures Customized for Formal Verification. CADE Randal E. Bryant, Sanjit A. Seshia
2005	—	`conf`	Modeling and Verifying Circuits Using Generalized Relative Timing. ASYNC Sanjit A. Seshia, Randal E. Bryant, Kenneth S. Stevens
2005	J	`jnl`	Modular verification of multithreaded programs. Theor. Comput. Sci. Cormac Flanagan, Stephen N. Freund, Shaz Qadeer, Sanjit A. Seshia
2005	—	`conf`	Semantics-Aware Malware Detection. S&P Mihai Christodorescu, Somesh Jha, Sanjit A. Seshia, Dawn Xiaodong Song, Randal E. Bryant
2004	A*	`conf`	Abstraction-Based Satisfiability Solving of Presburger Arithmetic. CAV Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman
2004	A*	`conf`	Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. LICS Sanjit A. Seshia, Randal E. Bryant
2004	A*	`conf`	The UCLID Decision Procedure. CAV Shuvendu K. Lahiri, Sanjit A. Seshia
2003	A*	`conf`	A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. DAC Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant
2003	—	`conf`	Convergence Testing in Term-Level Bounded Model Checking. CHARME Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
2003	A*	`conf`	Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. CAV Sanjit A. Seshia, Randal E. Bryant
2002	A*	`conf`	A Modular Checker for Multithreaded Programs. CAV Cormac Flanagan, Shaz Qadeer, Sanjit A. Seshia
2002	A*	`conf`	Deciding Separation Formulas with SAT. CAV Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant
2002	B	`conf`	Modeling and Verification of Out-of-Order Microprocessors in UCLID. FMCAD Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant
2002	A*	`conf`	Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. CAV Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
1999	B	`conf`	A Graphical Environment for the Specification and Verification of Reactive Systems. SAFECOMP A. K. Bhattacharjee, S. D. Dhodapkar, Sanjit A. Seshia, R. K. Shyamasundar
1999	—	`conf`	A Translation of Statecharts to Esterel. World Congress on Formal Methods Sanjit A. Seshia, R. K. Shyamasundar, A. K. Bhattacharjee, S. D. Dhodapkar