Sanjit A. Seshia
According to our database^{1},
Sanjit A. Seshia
authored at least 176 papers
between 1999 and 2019.
Collaborative distances:
Collaborative distances:
Awards
IEEE Fellow
IEEE Fellow 2018, "For contributions to formal methods for inductive synthesis and algorithmic verification".
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:

at orcid.org
On csauthors.net:
Bibliography
2019
A Formal Approach to Secure Speculation.
IACR Cryptology ePrint Archive, 2019
Scenic: a language for scenario specification and scene generation.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019
A new simulation metric to determine safe environments and controllers for systems with unknown dynamics.
Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019
2018
Modeling for Verification.
Proceedings of the Handbook of Model Checking., 2018
SMC: Satisfiability Modulo Convex Programming.
Proceedings of the IEEE, 2018
Compositional programming and testing of dynamic distributed systems.
PACMPL, 2018
Synthesis of Obfuscation Policies to Ensure Privacy and Utility.
J. Autom. Reasoning, 2018
Safe Autonomy Under Perception Uncertainty Using ChanceConstrained Temporal Logic.
J. Autom. Reasoning, 2018
Automatic Generation of Communication Requirements for Enforcing MultiAgent Safety.
Proceedings of the Proceedings 2nd International Workshop on Safe Control of Autonomous Vehicles, 2018
Toward an Internet of Battlefield Things: A Resilience Perspective.
IEEE Computer, 2018
Planning for cars that coordinate with people: leveraging effects on human actions for planning and active information gathering over human internal state.
Auton. Robots, 2018
TimeSeries Learning Using Monotonic Logical Properties.
Proceedings of the Runtime Verification  18th International Conference, 2018
Learning Task Specifications from Demonstrations.
Proceedings of the Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, 2018
A LiDAR Point Cloud Generator: from a Virtual World to Autonomous Driving.
Proceedings of the 2018 ACM on International Conference on Multimedia Retrieval, 2018
UCLID5: Integrating Modeling, Verification, Synthesis and Learning.
Proceedings of the 16th ACM/IEEE International Conference on Formal Methods and Models for System Design, 2018
Programming Safe Robotics Systems: Challenges and Advances.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification, 2018
CounterexampleGuided Data Augmentation.
Proceedings of the TwentySeventh International Joint Conference on Artificial Intelligence, 2018
Will Distributed Computing Revolutionize Peace? The Emergence of Battlefield IoT.
Proceedings of the 38th IEEE International Conference on Distributed Computing Systems, 2018
Understanding and Extending Incremental Determinization for 2QBF.
Proceedings of the Computer Aided Verification  30th International Conference, 2018
Reactive Control Improvisation.
Proceedings of the Computer Aided Verification  30th International Conference, 2018
Semantic Adversarial Deep Learning.
Proceedings of the Computer Aided Verification  30th International Conference, 2018
CyberPhysical Systems Education: Explorations and Dreams.
Proceedings of the Principles of Modeling, 2018
Formal Specification for Deep Neural Networks.
Proceedings of the Automated Technology for Verification and Analysis, 2018
Generating Dominant Strategies for Continuous TwoPlayer ZeroSum Games.
Proceedings of the 6th IFAC Conference on Analysis and Design of Hybrid Systems, 2018
2017
2016 IEEE Education Society Awards, 2016 Frontiers in Education Conference Awards, and Selected IEEE Awards.
IEEE Trans. Education, 2017
Design Automation of CyberPhysical Systems: Challenges, Advances, and Opportunities.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2017
Secure State Estimation for CyberPhysical Systems Under Sensor Attacks: A Satisfiability Modulo Theory Approach.
IEEE Trans. Automat. Contr., 2017
Program synthesis for interactivesecurity systems.
Formal Methods in System Design, 2017
Machine Learning and Formal Method (Dagstuhl Seminar 17351).
Dagstuhl Reports, 2017
Symbolic control design for monotone systems with directed specifications.
Automatica, 2017
A theory of formal synthesis via inductive learning.
Acta Inf., 2017
A compiler and verifier for page access oblivious computation.
Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, 2017
TeLEx: Passive STL Learning Using Only Positive Examples.
Proceedings of the Runtime Verification  17th International Conference, 2017
Combining Model Checking and Runtime Verification for Safe Robotics.
Proceedings of the Runtime Verification  17th International Conference, 2017
Active PreferenceBased Learning of Reward Functions.
Proceedings of the Robotics: Science and Systems XIII, 2017
Compositional Falsification of CyberPhysical Systems with Machine Learning Components.
Proceedings of the NASA Formal Methods  9th International Symposium, 2017
DRONA: a framework for safe distributed mobile robotics.
Proceedings of the 8th International Conference on CyberPhysical Systems, 2017
SMC: Satisfiability Modulo Convex Optimization.
Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, 2017
A Small Gain Theorem for Parametric AssumeGuarantee Contracts.
Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, 2017
Linear temporal logic motion planning for teams of underactuated robots using satisfiability modulo convex programming.
Proceedings of the 56th IEEE Annual Conference on Decision and Control, 2017
Dynamic contracts for distributed temporal logic control of traffic networks.
Proceedings of the 56th IEEE Annual Conference on Decision and Control, 2017
A Formal Foundation for Secure Remote Execution of Enclaves.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30, 2017
Logical Clustering and Learning for TimeSeries Data.
Proceedings of the Computer Aided Verification  29th International Conference, 2017
Stochastic predictive freeway ramp metering from Signal Temporal Logic specifications.
Proceedings of the 2017 American Control Conference, 2017
Maximum Model Counting.
Proceedings of the ThirtyFirst AAAI Conference on Artificial Intelligence, 2017
2016
Specification Mining for Machine Improvisation with Formal Specifications.
Computers in Entertainment, 2016
Incremental Determinization.
Proceedings of the Theory and Applications of Satisfiability Testing  SAT 2016, 2016
On the Hardness of SAT with Community Structure.
Proceedings of the Theory and Applications of Satisfiability Testing  SAT 2016, 2016
Planning for Autonomous Cars that Leverage Effects on Human Actions.
Proceedings of the Robotics: Science and Systems XII, University of Michigan, Ann Arbor, Michigan, USA, June 18, 2016
A design and verification methodology for secure isolated regions.
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016
Obfuscator Synthesis for Privacy and Utility.
Proceedings of the NASA Formal Methods  8th International Symposium, 2016
Towards trustworthy automation: User interfaces that convey internal and external awareness.
Proceedings of the 19th IEEE International Conference on Intelligent Transportation Systems, 2016
Learning and Visualizing Music Specifications Using Pattern Graphs.
Proceedings of the 17th International Society for Music Information Retrieval Conference, 2016
Information gathering actions over human internal state.
Proceedings of the 2016 IEEE/RSJ International Conference on Intelligent Robots and Systems, 2016
Control Improvisation with Probabilistic Temporal Specifications.
Proceedings of the First IEEE International Conference on InternetofThings Design and Implementation, 2016
SMTBased Observer Design for CyberPhysical Systems under Sensor Attacks.
Proceedings of the 7th ACM/IEEE International Conference on CyberPhysical Systems, 2016
Implan: Scalable Incremental Motion Planning for MultiRobot Systems.
Proceedings of the 7th ACM/IEEE International Conference on CyberPhysical Systems, 2016
Directed Specifications and Assumption Mining for Monotone Dynamical Systems.
Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, 2016
Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications.
Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, 2016
ddNF: An Efficient Data Structure for Header Spaces.
Proceedings of the Hardware and Software: Verification and Testing, 2016
Combining requirement mining, software model checking and simulationbased verification for industrial automotive systems.
Proceedings of the 2016 Formal Methods in ComputerAided Design, 2016
On ∃ ∀ ∃! solving: A case study on automated synthesis of magic card tricks.
Proceedings of the 2016 Formal Methods in ComputerAided Design, 2016
Scalable lazy SMTbased motion planning.
Proceedings of the 55th IEEE Conference on Decision and Control, 2016
Privacyaware quadratic optimization using partially homomorphic encryption.
Proceedings of the 55th IEEE Conference on Decision and Control, 2016
Assumeguarantee contracts and controller synthesis for vehicular traffic networks.
Proceedings of the 2016 American Control Conference, 2016
Constrained Sampling and Counting: Universal Hashing Meets SAT Solving.
Proceedings of the Beyond NP, 2016
2015
SyntaxGuided Synthesis.
Proceedings of the Dependable Software Systems Engineering, 2015
Combining Induction, Deduction, and Structure for Verification and Synthesis.
Proceedings of the IEEE, 2015
On Parallel Scalable Uniform SAT Witness Generation.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015
Systematic testing of asynchronous reactive systems.
Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, 2015
Robust Online Monitoring of Signal Temporal Logic.
Proceedings of the Runtime Verification  6th International Conference, 2015
ClusteringBased Active Learning for CPSGrader.
Proceedings of the Second ACM Conference on Learning @ Scale, 2015
Reactive synthesis from signal temporal logic specifications.
Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 2015
Control Improvisation.
Proceedings of the 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, 2015
Formal methods for semiautonomous driving.
Proceedings of the 52nd Annual Design Automation Conference, 2015
Secure state reconstruction in differentially flat systems under sensor attacks using satisfiability modulo theory solving.
Proceedings of the 54th IEEE Conference on Decision and Control, 2015
Compositional controller synthesis for vehicular traffic networks.
Proceedings of the 54th IEEE Conference on Decision and Control, 2015
Moat: Verifying Confidentiality of Enclave Programs.
Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, 2015
Approximate Synchrony: An Abstraction for Distributed AlmostSynchronous Systems.
Proceedings of the Computer Aided Verification  27th International Conference, 2015
Sound and complete state estimation for linear dynamical systems under sensor attacks using Satisfiability Modulo Theory solving.
Proceedings of the American Control Conference, 2015
Automotive systems requirement mining using breach.
Proceedings of the American Control Conference, 2015
2014
Reverse Engineering Digital Circuits Using Structural and Functional Analyses.
IEEE Trans. Emerging Topics Comput., 2014
Compositional Performance Verification of NetworkonChip Designs.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2014
The Swarm at the Edge of the Cloud.
IEEE Design & Test, 2014
Decision Procedures and Abstract Interpretation (Dagstuhl Seminar 14351).
Dagstuhl Reports, 2014
Are There Good Mistakes? A Theoretical Analysis of CEGIS.
Proceedings of the Proceedings 3rd Workshop on Synthesis, 2014
A ContractBased Methodology for Aircraft Electric Power System Design.
IEEE Access, 2014
Formal Modeling and Verification of CloudProxy.
Proceedings of the Verified Software: Theories, Tools and Experiments, 2014
Synthesis with Identifiers.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2014
Synthesis for HumanintheLoop Control Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014
Speeding Up SMTBased Quantitative Program Analysis.
Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, 2014
Distributed control of a swarm of buildings connected to a smart grid: demo abstract.
Proceedings of the 1st ACM Conference on Embedded Systems for EnergyEfficient Buildings, 2014
Automated composition of motion primitives for multirobot systems from safe LTL specifications.
Proceedings of the 2014 IEEE/RSJ International Conference on Intelligent Robots and Systems, 2014
Game theoretic secure localization in wireless sensor networks.
Proceedings of the 4th International Conference on the Internet of Things, 2014
Machine Improvisation with Formal Specifications.
Proceedings of the Music Technology meets Philosophy, 2014
Safety envelope for security.
Proceedings of the 3rd International Conference on High Confidence Networked Systems (part of CPS Week), 2014
User interface design and verification for semiautonomous driving.
Proceedings of the 3rd International Conference on High Confidence Networked Systems (part of CPS Week), 2014
Robust strategy synthesis for probabilistic systems applied to risklimiting renewableenergy pricing.
Proceedings of the 2014 International Conference on Embedded Software, 2014
CPSGrader: Synthesizing temporal logic testers for autograding an embedded systems laboratory.
Proceedings of the 2014 International Conference on Embedded Software, 2014
A learning based approach to control synthesis of Markov decision processes for linear temporal logic specifications.
Proceedings of the 53rd IEEE Conference on Decision and Control, 2014
Model predictive control with signal temporal logic specifications.
Proceedings of the 53rd IEEE Conference on Decision and Control, 2014
DataDriven Probabilistic Modeling and Verification of Human Driver Behavior.
Proceedings of the 2014 AAAI Spring Symposia, 2014
DistributionAware Sampling and Weighted Model Counting for SAT.
Proceedings of the TwentyEighth AAAI Conference on Artificial Intelligence, 2014
2013
Symbolic software model validation.
Proceedings of the 11th ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2013
Verifying HighConfidence Interactive Systems: Electronic Voting and Beyond.
Proceedings of the Distributed Computing and Networking, 14th International Conference, 2013
Mining requirements from closedloop control models.
Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013
WordRev: Finding wordlevel structures in a sea of bitlevel gates.
Proceedings of the 2013 IEEE International Symposium on HardwareOriented Security and Trust, 2013
Syntaxguided synthesis.
Proceedings of the Formal Methods in ComputerAided Design, 2013
Synthesis of Implementable Control Strategies for Lazy Linear Hybrid Automata.
Proceedings of the 2013 Federated Conference on Computer Science and Information Systems, 2013
PolynomialTime Verification of PCTL Properties of MDPs with Convex Uncertainties.
Proceedings of the Computer Aided Verification  25th International Conference, 2013
2012
Quantitative Analysis of Systems Using GameTheoretic Learning.
ACM Trans. Embedded Comput. Syst., 2012
Distributed RealTime Software for CyberPhysical Systems.
Proceedings of the IEEE, 2012
Sparse Coding for Specification Mining and Error Localization.
Proceedings of the Runtime Verification, Third International Conference, 2012
Compositional performance verification of NoC designs.
Proceedings of the Tenth ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2012
Reverse engineering circuits using behavioral pattern mining.
Proceedings of the 2012 IEEE International Symposium on HardwareOriented Security and Trust, 2012
Verification with small and short worlds.
Proceedings of the Formal Methods in ComputerAided Design, 2012
Automating exercise generation: a step towards meeting the MOOC challenge for embedded systems.
Proceedings of the Workshop on Embedded and CyberPhysical Systems Education, 2012
Teaching embedded systems the Berkeley way.
Proceedings of the Workshop on Embedded and CyberPhysical Systems Education, 2012
Sciduction: combining induction, deduction, and structure for verification and synthesis.
Proceedings of the 49th Annual Design Automation Conference 2012, 2012
CrowdMine: towards crowdsourced humanassisted verification.
Proceedings of the 49th Annual Design Automation Conference 2012, 2012
2011
GameTime: A Toolkit for Timing Analysis of Software.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011
Mining assumptions for synthesis.
Proceedings of the 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, 2011
An introductory capstone design course on embedded systems.
Proceedings of the International Symposium on Circuits and Systems (ISCAS 2011), 2011
Synthesis with Clairvoyance.
Proceedings of the Hardware and Software: Verification and Testing, 2011
Timing analysis of interruptdriven programs under context bounds.
Proceedings of the International Conference on Formal Methods in ComputerAided Design, 2011
Learning conditional abstractions.
Proceedings of the International Conference on Formal Methods in ComputerAided Design, 2011
Synthesis of optimal switching logic for hybrid systems.
Proceedings of the 11th International Conference on Embedded Software, 2011
Counterexampleguided SMTdriven optimal buffer sizing.
Proceedings of the Design, Automation and Test in Europe, 2011
Abstractionbased performance verification of NoCs.
Proceedings of the 48th Design Automation Conference, 2011
2010
ATLAS: Automatic Termlevel abstraction of RTL designs.
Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010
Oracleguided componentbased program synthesis.
Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010
Synthesizing switching logic for safety and dwelltime requirements.
Proceedings of the ACM/IEEE 1st International Conference on CyberPhysical Systems, 2010
CalCS: SMT solving for nonlinear convex constraints.
Proceedings of 10th International Conference on Formal Methods in ComputerAided Design, 2010
Quantitative Analysis of Software: Challenges and Recent Advances.
Proceedings of the Formal Aspects of Component Software  7th International Workshop, 2010
An introductory textbook on cyberphysical systems.
Proceedings of the 2010 Workshop on Embedded Systems Education, 2010
Automating Security Mediation Placement.
Proceedings of the Programming Languages and Systems, 2010
Postsilicon validation opportunities, challenges and recent advances.
Proceedings of the 47th Design Automation Conference, 2010
Scalable specification mining for verification and diagnosis.
Proceedings of the 47th Design Automation Conference, 2010
2009
Satisfiability Modulo Theories.
Proceedings of the Handbook of Satisfiability, 2009
An abstractionbased decision procedure for bitvector arithmetic.
STTT, 2009
The Case for TimingCentric Distributed Software Invited Paper.
Proceedings of the 29th IEEE International Conference on Distributed Computing Systems Workshops (ICDCS 2009 Workshops), 2009
Localizing transient faults using dynamic bayesian networks.
Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2009
Optimizations of an applicationlevel protocol for enhanced dependability in FlexRay.
Proceedings of the Design, Automation and Test in Europe, 2009
Design as you see FIT: Systemlevel soft error analysis of sequential circuits.
Proceedings of the Design, Automation and Test in Europe, 2009
On voting machine design for verification and testability.
Proceedings of the 2009 ACM Conference on Computer and Communications Security, 2009
Beaver: Engineering an Efficient SMT Solver for BitVector Arithmetic.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009
2008
Effective blame for informationflow violations.
Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2008
Gametheoretic timing analysis.
Proceedings of the 2008 International Conference on ComputerAided Design, 2008
A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance.
Proceedings of the Formal Methods in ComputerAided Design, 2008
2007
On Solving Boolean Combinations of UTVPI Constraints.
JSAT, 2007
Deciding BitVector Arithmetic with Abstraction.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007
Sketching stencils.
Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007
An Application ofWebService Interfaces.
Proceedings of the 2007 IEEE International Conference on Web Services (ICWS 2007), 2007
Formal verification at higher levels of abstraction.
Proceedings of the 2007 International Conference on ComputerAided Design, 2007
Autonomic Reactive Systems via Online Learning.
Proceedings of the Fourth International Conference on Autonomic Computing (ICAC'07), 2007
Symbolic Reachability Analysis of Lazy Linear Hybrid Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2007
Verificationguided soft error resilience.
Proceedings of the 2007 Design, Automation and Test in Europe Conference and Exposition, 2007
Interactive presentation: Automatic model generation for black box realtime systems.
Proceedings of the 2007 Design, Automation and Test in Europe Conference and Exposition, 2007
2006
Combinatorial sketching for finite programs.
Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, 2006
2005
Modular verification of multithreaded programs.
Theor. Comput. Sci., 2005
SemanticsAware Malware Detection.
Proceedings of the 2005 IEEE Symposium on Security and Privacy (S&P 2005), 2005
Automatic discovery of APIlevel exploits.
Proceedings of the 27th International Conference on Software Engineering (ICSE 2005), 2005
Decision Procedures Customized for Formal Verification.
Proceedings of the Automated Deduction, 2005
Modeling and Verifying Circuits Using Generalized Relative Timing.
Proceedings of the 11th International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 2005), 2005
2004
Deciding QuantifierFree Presburger Formulas Using Parameterized Solution Bounds.
Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004
The UCLID Decision Procedure.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004
AbstractionBased Satisfiability Solving of Presburger Arithmetic.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004
2003
A hybrid SATbased decision procedure for separation logic with uninterpreted functions.
Proceedings of the 40th Design Automation Conference, 2003
Convergence Testing in TermLevel Bounded Model Checking.
Proceedings of the Correct Hardware Design and Verification Methods, 2003
Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003
2002
Modeling and Verification of OutofOrder Microprocessors in UCLID.
Proceedings of the Formal Methods in ComputerAided Design, 4th International Conference, 2002
Deciding Separation Formulas with SAT.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002
A Modular Checker for Multithreaded Programs.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002
Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002
1999
A Graphical Environment for the Specification and Verification of Reactive Systems.
Proceedings of the Computer Safety, 1999
A Translation of Statecharts to Esterel.
Proceedings of the FM'99  Formal Methods, 1999