Sanjit A. Seshia

According to our database1, Sanjit A. Seshia
  • authored at least 179 papers between 1999 and 2017.
  • has a "Dijkstra number"2 of three.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepage:

On csauthors.net:

Bibliography

2017
2016 IEEE Education Society Awards, 2016 Frontiers in Education Conference Awards, and Selected IEEE Awards.
IEEE Trans. Education, 2017

Design Automation of Cyber-Physical Systems: Challenges, Advances, and Opportunities.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2017

Secure State Estimation for Cyber-Physical Systems Under Sensor Attacks: A Satisfiability Modulo Theory Approach.
IEEE Trans. Automat. Contr., 2017

A Formal Foundation for Secure Remote Execution of Enclaves.
IACR Cryptology ePrint Archive, 2017

Program synthesis for interactive-security systems.
Formal Methods in System Design, 2017

Robust online monitoring of signal temporal logic.
Formal Methods in System Design, 2017

Specification Inference from Demonstrations.
CoRR, 2017

Systematic Testing of Convolutional Neural Networks for Autonomous Driving.
CoRR, 2017

Tunable Reactive Synthesis for Lipschitz-Bounded Systems with Temporal Logic Specifications.
CoRR, 2017

Model Predictive Control for Signal Temporal Logic Specification.
CoRR, 2017

Control Improvisation.
CoRR, 2017

Compositional Falsification of Cyber-Physical Systems with Machine Learning Components.
CoRR, 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

Compositional Falsification of Cyber-Physical 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 Cyber-Physical 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 Assume-Guarantee Contracts.
Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, 2017

A Formal Foundation for Secure Remote Execution of Enclaves.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017

Logical Clustering and Learning for Time-Series 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 Thirty-First AAAI Conference on Artificial Intelligence, 2017

2016
Learning Auditable Features from Signals Using Unsupervised Temporal Projection.
CoRR, 2016

Towards Verified Artificial Intelligence.
CoRR, 2016

On the Hardness of SAT with Community Structure.
CoRR, 2016

Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications.
CoRR, 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 Internet-of-Things Design and Implementation, 2016

SMT-Based Observer Design for Cyber-Physical Systems under Sensor Attacks.
Proceedings of the 7th ACM/IEEE International Conference on Cyber-Physical Systems, 2016

Implan: Scalable Incremental Motion Planning for Multi-Robot Systems.
Proceedings of the 7th ACM/IEEE International Conference on Cyber-Physical 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 simulation-based verification for industrial automotive systems.
Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

On ∃ ∀ ∃! solving: A case study on automated synthesis of magic card tricks.
Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

Scalable lazy SMT-based motion planning.
Proceedings of the 55th IEEE Conference on Decision and Control, 2016

Privacy-aware quadratic optimization using partially homomorphic encryption.
Proceedings of the 55th IEEE Conference on Decision and Control, 2016

Assume-guarantee 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

Mining Requirements From Closed-Loop Control Models.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2015

Combining Induction, Deduction, and Structure for Verification and Synthesis.
Proceedings of the IEEE, 2015

A Satisfiability Modulo Theory Approach to Secure State Reconstruction in Differentially Flat Systems Under Sensor Attacks.
CoRR, 2015

Constrained Sampling and Counting: Universal Hashing Meets SAT Solving.
CoRR, 2015

A Theory of Formal Synthesis via Inductive Learning.
CoRR, 2015

Robust Online Monitoring of Signal Temporal Logic.
CoRR, 2015

What's Decidable about Syntax-Guided Synthesis?
CoRR, 2015

On Systematic Testing for Execution-Time Analysis.
CoRR, 2015

Control Improvisation with Probabilistic Temporal Specifications.
CoRR, 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

Clustering-Based 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 semi-autonomous 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 Almost-Synchronous 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 Network-on-Chip 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

Secure State Estimation Under Sensor Attacks: A Satisfiability Modulo Theory Approach.
CoRR, 2014

A Learning Based Approach to Control Synthesis of Markov Decision Processes for Linear Temporal Logic Specifications.
CoRR, 2014

Are There Good Mistakes? A Theoretical Analysis of CEGIS.
Proceedings of the Proceedings 3rd Workshop on Synthesis, 2014

Speeding Up SMT-Based Quantitative Program Analysis.
CoRR, 2014

Control Improvisation.
CoRR, 2014

Distribution-Aware Sampling and Weighted Model Counting for SAT.
CoRR, 2014

A Contract-Based 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 Human-in-the-Loop Control Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Speeding Up SMT-Based 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 Energy-Efficient Buildings, 2014

Automated composition of motion primitives for multi-robot 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 semi-autonomous 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 risk-limiting renewable-energy pricing.
Proceedings of the 2014 International Conference on Embedded Software, 2014

CPSGrader: Synthesizing temporal logic testers for auto-grading 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

Distribution-Aware Sampling and Weighted Model Counting for SAT.
Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, 2014

2013
SWATI: Synthesizing Wordlengths Automatically Using Testing and Induction
CoRR, 2013

Robust Subspace System Identification via Weighted Nuclear Norm Optimization.
CoRR, 2013

Symbolic software model validation.
Proceedings of the 11th ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2013

Verifying High-Confidence Interactive Systems: Electronic Voting and Beyond.
Proceedings of the Distributed Computing and Networking, 14th International Conference, 2013

Mining requirements from closed-loop control models.
Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013

WordRev: Finding word-level structures in a sea of bit-level gates.
Proceedings of the 2013 IEEE International Symposium on Hardware-Oriented Security and Trust, 2013

Syntax-guided synthesis.
Proceedings of the Formal Methods in Computer-Aided 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

Polynomial-Time 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 Game-Theoretic Learning.
ACM Trans. Embedded Comput. Syst., 2012

Distributed Real-Time Software for Cyber-Physical Systems.
Proceedings of the IEEE, 2012

Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis
CoRR, 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 Hardware-Oriented Security and Trust, 2012

Verification with small and short worlds.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

Automating exercise generation: a step towards meeting the MOOC challenge for embedded systems.
Proceedings of the Workshop on Embedded and Cyber-Physical Systems Education, 2012

Teaching embedded systems the Berkeley way.
Proceedings of the Workshop on Embedded and Cyber-Physical 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 human-assisted verification.
Proceedings of the 49th Annual Design Automation Conference 2012, 2012

2011
Synthesizing Switching Logic to Minimize Long-Run Cost
CoRR, 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 interrupt-driven programs under context bounds.
Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

Learning conditional abstractions.
Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

Synthesis of optimal switching logic for hybrid systems.
Proceedings of the 11th International Conference on Embedded Software, 2011

Counterexample-guided SMT-driven optimal buffer sizing.
Proceedings of the Design, Automation and Test in Europe, 2011

Abstraction-based performance verification of NoCs.
Proceedings of the 48th Design Automation Conference, 2011

2010
ATLAS: Automatic Term-level abstraction of RTL designs.
Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010

Oracle-guided component-based program synthesis.
Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010

Synthesizing switching logic for safety and dwell-time requirements.
Proceedings of the ACM/IEEE 1st International Conference on Cyber-Physical Systems, 2010

CalCS: SMT solving for non-linear convex constraints.
Proceedings of 10th International Conference on Formal Methods in Computer-Aided 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 cyber-physical systems.
Proceedings of the 2010 Workshop on Embedded Systems Education, 2010

Automating Security Mediation Placement.
Proceedings of the Programming Languages and Systems, 2010

Post-silicon 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 abstraction-based decision procedure for bit-vector arithmetic.
STTT, 2009

On the Computational Complexity of Satisfiability Solving for String Theories
CoRR, 2009

The Case for Timing-Centric 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 application-level protocol for enhanced dependability in FlexRay.
Proceedings of the Design, Automation and Test in Europe, 2009

Design as you see FIT: System-level 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 Bit-Vector Arithmetic.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008
Effective blame for information-flow violations.
Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2008

Game-theoretic timing analysis.
Proceedings of the 2008 International Conference on Computer-Aided Design, 2008

A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance.
Proceedings of the Formal Methods in Computer-Aided Design, 2008

2007
On Solving Boolean Combinations of UTVPI Constraints.
JSAT, 2007

Deciding Bit-Vector 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 ofWeb-Service 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 Computer-Aided 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

Verification-guided 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 real-time 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

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds.
Logical Methods in Computer Science, 2005

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
CoRR, 2005

Semantics-Aware Malware Detection.
Proceedings of the 2005 IEEE Symposium on Security and Privacy (S&P 2005), 2005

Automatic discovery of API-level 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 Quantifier-Free 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

Abstraction-Based Satisfiability Solving of Presburger Arithmetic.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003
A hybrid SAT-based decision procedure for separation logic with uninterpreted functions.
Proceedings of the 40th Design Automation Conference, 2003

Convergence Testing in Term-Level 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 Out-of-Order Microprocessors in UCLID.
Proceedings of the Formal Methods in Computer-Aided 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


  Loading...