Sanjit A. Seshia

Nick Landolfi

Shankar S. Sastry

Anca D. Dragan

Auton. Robots, 2018

Time-Series Learning Using Monotonic Logical Properties.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 18th International Conference, 2018

Learning Task Specifications from Demonstrations.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the 2018 ACM on International Conference on Multimedia Retrieval, 2018

UCLID5: Integrating Modeling, Verification, Synthesis and Learning.

[BibT_eX]

[DOI]

Pramod Subramanyan

Proceedings of the 16th ACM/IEEE International Conference on Formal Methods and Models for System Design, 2018

Programming Safe Robotics Systems: Challenges and Advances.

[BibT_eX]

[DOI]

Ankush Desai

Shaz Qadeer

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification, 2018

Counterexample-Guided Data Augmentation.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018

Will Distributed Computing Revolutionize Peace? The Emergence of Battlefield IoT.

[BibT_eX]

[DOI]

Proceedings of the 38th IEEE International Conference on Distributed Computing Systems, 2018

Understanding and Extending Incremental Determinization for 2QBF.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Reactive Control Improvisation.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Cyber-Physical Systems Education: Explorations and Dreams.

[BibT_eX]

[DOI]

Proceedings of the Principles of Modeling, 2018

Formal Specification for Deep Neural Networks.

[BibT_eX]

[DOI]

Xiangyu Yue

Proceedings of the Automated Technology for Verification and Analysis, 2018

Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games.

[BibT_eX]

[DOI]

Vasumathi Raman

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.

[BibT_eX]

[DOI]

IEEE Trans. Educ., 2017

Design Automation of Cyber-Physical Systems: Challenges, Advances, and Opportunities.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2017

Secure State Estimation for Cyber-Physical Systems Under Sensor Attacks: A Satisfiability Modulo Theory Approach.

[BibT_eX]

[DOI]

IEEE Trans. Autom. Control., 2017

A Formal Foundation for Secure Remote Execution of Enclaves.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2017

Program synthesis for interactive-security systems.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2017

Robust online monitoring of signal temporal logic.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2017

Machine Learning and Formal Method (Dagstuhl Seminar 17351).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2017

Specification Inference from Demonstrations.

[BibT_eX]

[DOI]

Ashish Tiwari

CoRR, 2017

Systematic Testing of Convolutional Neural Networks for Autonomous Driving.

[BibT_eX]

[DOI]

Tommaso Dreossi

CoRR, 2017

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

[BibT_eX]

[DOI]

Vasumathi Raman

CoRR, 2017

Model Predictive Control for Signal Temporal Logic Specification.

[BibT_eX]

[DOI]

CoRR, 2017

Control Improvisation.

[BibT_eX]

[DOI]

CoRR, 2017

Symbolic control design for monotone systems with directed specifications.

[BibT_eX]

[DOI]

Autom., 2017

A theory of formal synthesis via inductive learning.

[BibT_eX]

[DOI]

Acta Informatica, 2017

A compiler and verifier for page access oblivious computation.

[BibT_eX]

[DOI]

Rohit Sinha

Sriram K. Rajamani

Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, 2017

TeLEx: Passive STL Learning Using Only Positive Examples.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 17th International Conference, 2017

Combining Model Checking and Runtime Verification for Safe Robotics.

[BibT_eX]

[DOI]

Ankush Desai

Tommaso Dreossi

Proceedings of the Runtime Verification - 17th International Conference, 2017

Active Preference-Based Learning of Reward Functions.

[BibT_eX]

[DOI]

Proceedings of the Robotics: Science and Systems XIII, 2017

DRONA: a framework for safe distributed mobile robotics.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on Cyber-Physical Systems, 2017

SMC: Satisfiability Modulo Convex Optimization.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, 2017

A Small Gain Theorem for Parametric Assume-Guarantee Contracts.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the 56th IEEE Annual Conference on Decision and Control, 2017

Dynamic contracts for distributed temporal logic control of traffic networks.

[BibT_eX]

[DOI]

Proceedings of the 56th IEEE Annual Conference on Decision and Control, 2017

Logical Clustering and Learning for Time-Series Data.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Stochastic predictive freeway ramp metering from Signal Temporal Logic specifications.

[BibT_eX]

[DOI]

Proceedings of the 2017 American Control Conference, 2017

Maximum Model Counting.

[BibT_eX]

[DOI]

Markus N. Rabe

Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, 2017

2016

Learning Auditable Features from Signals Using Unsupervised Temporal Projection.

[BibT_eX]

[DOI]

Marcell V.-Chanlatte

CoRR, 2016

Towards Verified Artificial Intelligence.

[BibT_eX]

[DOI]

CoRR, 2016

Specification Mining for Machine Improvisation with Formal Specifications.

[BibT_eX]

[DOI]

Comput. Entertain., 2016

Incremental Determinization.

[BibT_eX]

[DOI]

Markus N. Rabe

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

On the Hardness of SAT with Community Structure.

[BibT_eX]

[DOI]

Nathan Mull

Katherine Rose Driggs-Campbell

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

Planning for Autonomous Cars that Leverage Effects on Human Actions.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

Obfuscator Synthesis for Privacy and Utility.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

Towards trustworthy automation: User interfaces that convey internal and external awareness.

[BibT_eX]

[DOI]

Tara Rezvani

Proceedings of the 19th IEEE International Conference on Intelligent Transportation Systems, 2016

Learning and Visualizing Music Specifications Using Pattern Graphs.

[BibT_eX]

[DOI]

Proceedings of the 17th International Society for Music Information Retrieval Conference, 2016

Information gathering actions over human internal state.

[BibT_eX]

[DOI]

Proceedings of the 2016 IEEE/RSJ International Conference on Intelligent Robots and Systems, 2016

Control Improvisation with Probabilistic Temporal Specifications.

[BibT_eX]

[DOI]

Proceedings of the First IEEE International Conference on Internet-of-Things Design and Implementation, 2016

Implan: Scalable Incremental Motion Planning for Multi-Robot Systems.

[BibT_eX]

[DOI]

Indranil Saha

Rattanachai Ramaithitima

Vijay Kumar

Proceedings of the 7th ACM/IEEE International Conference on Cyber-Physical Systems, 2016

Directed Specifications and Assumption Mining for Monotone Dynamical Systems.

[BibT_eX]

[DOI]

Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, 2016

Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications.

[BibT_eX]

[DOI]

Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, 2016

ddNF: An Efficient Data Structure for Header Spaces.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2016

Combining requirement mining, software model checking and simulation-based verification for industrial automotive systems.

[BibT_eX]

[DOI]

Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

On ∃ ∀ ∃! solving: A case study on automated synthesis of magic card tricks.

[BibT_eX]

[DOI]

Vasumathi Raman

Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

Scalable lazy SMT-based motion planning.

[BibT_eX]

[DOI]

Indranil Saha

Proceedings of the 55th IEEE Conference on Decision and Control, 2016

Privacy-aware quadratic optimization using partially homomorphic encryption.

[BibT_eX]

[DOI]

Proceedings of the 55th IEEE Conference on Decision and Control, 2016

Assume-guarantee contracts and controller synthesis for vehicular traffic networks.

[BibT_eX]

[DOI]

Proceedings of the 2016 American Control Conference, 2016

Constrained Sampling and Counting: Universal Hashing Meets SAT Solving.

[BibT_eX]

[DOI]

Proceedings of the Beyond NP, 2016

2015

Syntax-Guided Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Dependable Software Systems Engineering, 2015

Mining Requirements From Closed-Loop Control Models.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2015

Combining Induction, Deduction, and Structure for Verification and Synthesis.

[BibT_eX]

[DOI]

Proc. IEEE, 2015

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

[BibT_eX]

[DOI]

Nicola Bezzo

CoRR, 2015

What's Decidable about Syntax-Guided Synthesis?

[BibT_eX]

[DOI]

CoRR, 2015

On Systematic Testing for Execution-Time Analysis.

[BibT_eX]

[DOI]

Daniel Bundala

CoRR, 2015

On Parallel Scalable Uniform SAT Witness Generation.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Systematic testing of asynchronous reactive systems.

[BibT_eX]

[DOI]

Ankush Desai

Shaz Qadeer

Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, 2015

Clustering-Based Active Learning for CPSGrader.

[BibT_eX]

[DOI]

Proceedings of the Second ACM Conference on Learning @ Scale, 2015

Reactive synthesis from signal temporal logic specifications.

[BibT_eX]

[DOI]

Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 2015

Control Improvisation.

[BibT_eX]

[DOI]

Proceedings of the 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, 2015

Formal methods for semi-autonomous driving.

[BibT_eX]

[DOI]

Proceedings of the 52nd Annual Design Automation Conference, 2015

Secure state reconstruction in differentially flat systems under sensor attacks using satisfiability modulo theory solving.

[BibT_eX]

[DOI]

Nicola Bezzo

Proceedings of the 54th IEEE Conference on Decision and Control, 2015

Compositional controller synthesis for vehicular traffic networks.

[BibT_eX]

[DOI]

Proceedings of the 54th IEEE Conference on Decision and Control, 2015

Moat: Verifying Confidentiality of Enclave Programs.

[BibT_eX]

[DOI]

Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, 2015

Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the American Control Conference, 2015

Automotive systems requirement mining using breach.

[BibT_eX]

[DOI]

Proceedings of the American Control Conference, 2015

2014

Reverse Engineering Digital Circuits Using Structural and Functional Analyses.

[BibT_eX]

[DOI]

IEEE Trans. Emerg. Top. Comput., 2014

Compositional Performance Verification of Network-on-Chip Designs.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2014

The Swarm at the Edge of the Cloud.

[BibT_eX]

[DOI]

IEEE Des. Test, 2014

Decision Procedures and Abstract Interpretation (Dagstuhl Seminar 14351).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2014

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

[BibT_eX]

[DOI]

CoRR, 2014

Are There Good Mistakes? A Theoretical Analysis of CEGIS.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 3rd Workshop on Synthesis, 2014

A Contract-Based Methodology for Aircraft Electric Power System Design.

[BibT_eX]

[DOI]

Richard M. Murray

IEEE Access, 2014

Formal Modeling and Verification of CloudProxy.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

Synthesis with Identifiers.

[BibT_eX]

[DOI]

Rüdiger Ehlers

Hadas Kress-Gazit

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2014

Synthesis for Human-in-the-Loop Control Systems.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Speeding Up SMT-Based Quantitative Program Analysis.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Tajana Simunic Rosing

Jagannathan Venkatesh

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.

[BibT_eX]

[DOI]

Indranil Saha

Rattanachai Ramaithitima

Vijay Kumar

Proceedings of the 2014 IEEE/RSJ International Conference on Intelligent Robots and Systems, 2014

Game theoretic secure localization in wireless sensor networks.

[BibT_eX]

[DOI]

Stavros Tripakis

Krishnendu Chatterjee

Proceedings of the 4th International Conference on the Internet of Things, 2014

Machine Improvisation with Formal Specifications.

[BibT_eX]

[DOI]

Proceedings of the Music Technology meets Philosophy, 2014

Safety envelope for security.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Katherine Rose Driggs-Campbell

Ruzena Bajcsy

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.

[BibT_eX]

[DOI]

Proceedings of the 2014 International Conference on Embedded Software, 2014

CPSGrader: Synthesizing temporal logic testers for auto-grading an embedded systems laboratory.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the 53rd IEEE Conference on Decision and Control, 2014

Model predictive control with signal temporal logic specifications.

[BibT_eX]

[DOI]

Proceedings of the 53rd IEEE Conference on Decision and Control, 2014

Data-Driven Probabilistic Modeling and Verification of Human Driver Behavior.

[BibT_eX]

[DOI]

Katherine Rose Driggs-Campbell

Proceedings of the 2014 AAAI Spring Symposia, 2014

Distribution-Aware Sampling and Weighted Model Counting for SAT.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, 2014

2013

SWATI: Synthesizing Wordlengths Automatically Using Testing and Induction

[BibT_eX]

[DOI]

CoRR, 2013

Robust Subspace System Identification via Weighted Nuclear Norm Optimization.

[BibT_eX]

[DOI]

CoRR, 2013

Symbolic software model validation.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Distributed Computing and Networking, 14th International Conference, 2013

WordRev: Finding word-level structures in a sea of bit-level gates.

[BibT_eX]

[DOI]

Proceedings of the 2013 IEEE International Symposium on Hardware-Oriented Security and Trust, 2013

Syntax-guided synthesis.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2013

Synthesis of Implementable Control Strategies for Lazy Linear Hybrid Automata.

[BibT_eX]

[DOI]

Luigi Di Guglielmo

Tiziano Villa

Proceedings of the 2013 Federated Conference on Computer Science and Information Systems, 2013

Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012

Quantitative Analysis of Systems Using Game-Theoretic Learning.

[BibT_eX]

[DOI]

Alexander Rakhlin

ACM Trans. Embed. Comput. Syst., 2012

Distributed Real-Time Software for Cyber-Physical Systems.

[BibT_eX]

[DOI]

Proc. IEEE, 2012

Sparse Coding for Specification Mining and Error Localization.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification, Third International Conference, 2012

Compositional performance verification of NoC designs.

[BibT_eX]

[DOI]

Proceedings of the Tenth ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2012

Reverse engineering circuits using behavioral pattern mining.

[BibT_eX]

[DOI]

Zach Wasson

Proceedings of the 2012 IEEE International Symposium on Hardware-Oriented Security and Trust, 2012

Verification with small and short worlds.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2012

Automating exercise generation: a step towards meeting the MOOC challenge for embedded systems.

[BibT_eX]

[DOI]

Mona Gupta

Proceedings of the Workshop on Embedded and Cyber-Physical Systems Education, 2012

Teaching embedded systems the Berkeley way.

[BibT_eX]

[DOI]

Edward A. Lee

Jeff C. Jensen

Proceedings of the Workshop on Embedded and Cyber-Physical Systems Education, 2012

Sciduction: combining induction, deduction, and structure for verification and synthesis.

[BibT_eX]

[DOI]

Proceedings of the 49th Annual Design Automation Conference 2012, 2012

CrowdMine: towards crowdsourced human-assisted verification.

[BibT_eX]

[DOI]

Somesh Jha

Proceedings of the 49th Annual Design Automation Conference 2012, 2012

2011

Synthesizing Switching Logic to Minimize Long-Run Cost

[BibT_eX]

[DOI]

Ashish Tiwari

CoRR, 2011

GameTime: A Toolkit for Timing Analysis of Software.

[BibT_eX]

[DOI]

Jonathan Kotker

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Mining assumptions for synthesis.

[BibT_eX]

[DOI]

Lili Dworkin

Proceedings of the 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, 2011

An introductory capstone design course on embedded systems.

[BibT_eX]

[DOI]

Jeff C. Jensen

Edward A. Lee

Proceedings of the International Symposium on Circuits and Systems (ISCAS 2011), 2011

Synthesis with Clairvoyance.

[BibT_eX]

[DOI]

Orna Kupferman

Proceedings of the Hardware and Software: Verification and Testing, 2011

Timing analysis of interrupt-driven programs under context bounds.

[BibT_eX]

[DOI]

Jonathan Kotker

Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

Learning conditional abstractions.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

Synthesis of optimal switching logic for hybrid systems.

[BibT_eX]

[DOI]

Ashish Tiwari

Proceedings of the 11th International Conference on Embedded Software, 2011

Counterexample-guided SMT-driven optimal buffer sizing.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation and Test in Europe, 2011

Abstraction-based performance verification of NoCs.

[BibT_eX]

[DOI]

Proceedings of the 48th Design Automation Conference, 2011

2010

ATLAS: Automatic Term-level abstraction of RTL designs.

[BibT_eX]

[DOI]

Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010

Oracle-guided component-based program synthesis.

[BibT_eX]

[DOI]

Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010

Synthesizing switching logic for safety and dwell-time requirements.

[BibT_eX]

[DOI]

Proceedings of the ACM/IEEE 1st International Conference on Cyber-Physical Systems, 2010

CalCS: SMT solving for non-linear convex constraints.

[BibT_eX]

[DOI]

Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

Quantitative Analysis of Software: Challenges and Recent Advances.

[BibT_eX]

[DOI]

Proceedings of the Formal Aspects of Component Software - 7th International Workshop, 2010

An introductory textbook on cyber-physical systems.

[BibT_eX]

[DOI]

Edward A. Lee

Proceedings of the 2010 Workshop on Embedded Systems Education, 2010

Automating Security Mediation Placement.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2010

Post-silicon validation opportunities, challenges and recent advances.

[BibT_eX]

[DOI]

Subhasish Mitra

Nicola Nicolici

Proceedings of the 47th Design Automation Conference, 2010

Scalable specification mining for verification and diagnosis.

[BibT_eX]

[DOI]

Alessandro Forin

Proceedings of the 47th Design Automation Conference, 2010

2009

Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability, 2009

An abstraction-based decision procedure for bit-vector arithmetic.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2009

On the Computational Complexity of Satisfiability Solving for String Theories

[BibT_eX]

[DOI]

Rhishikesh Limaye

CoRR, 2009

The Case for Timing-Centric Distributed Software Invited Paper.

[BibT_eX]

[DOI]

Proceedings of the 29th IEEE International Conference on Distributed Computing Systems Workshops (ICDCS 2009 Workshops), 2009

Localizing transient faults using dynamic bayesian networks.

[BibT_eX]

[DOI]

Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2009

Optimizations of an application-level protocol for enhanced dependability in FlexRay.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation and Test in Europe, 2009

Design as you see FIT: System-level soft error analysis of sequential circuits.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation and Test in Europe, 2009

On voting machine design for verification and testability.

[BibT_eX]

[DOI]

Proceedings of the 2009 ACM Conference on Computer and Communications Security, 2009

Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic.

[BibT_eX]

[DOI]

Rhishikesh Limaye

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008

Effective blame for information-flow violations.

[BibT_eX]

[DOI]

Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2008

Game-theoretic timing analysis.

[BibT_eX]

[DOI]

Alexander Rakhlin

Proceedings of the 2008 International Conference on Computer-Aided Design, 2008

A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance.

[BibT_eX]

[DOI]

Orna Kupferman

Proceedings of the Formal Methods in Computer-Aided Design, 2008

2007

On Solving Boolean Combinations of UTVPI Constraints.

[BibT_eX]

[DOI]

K. Subramani

J. Satisf. Boolean Model. Comput., 2007

Deciding Bit-Vector Arithmetic with Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Sketching stencils.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

An Application ofWeb-Service Interfaces.

[BibT_eX]

[DOI]

Proceedings of the 2007 IEEE International Conference on Web Services (ICWS 2007), 2007

Formal verification at higher levels of abstraction.

[BibT_eX]

[DOI]

Daniel Kroening

Proceedings of the 2007 International Conference on Computer-Aided Design, 2007

Autonomic Reactive Systems via Online Learning.

[BibT_eX]

[DOI]

Proceedings of the Fourth International Conference on Autonomic Computing (ICAC'07), 2007

Symbolic Reachability Analysis of Lazy Linear Hybrid Automata.

[BibT_eX]

[DOI]

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2007

Verification-guided soft error resilience.

[BibT_eX]

[DOI]

Subhasish Mitra

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.

[BibT_eX]

[DOI]

Proceedings of the 2007 Design, Automation and Test in Europe Conference and Exposition, 2007

2006

Combinatorial sketching for finite programs.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, 2006

2005

Modular verification of multithreaded programs.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2005

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2005

Semantics-Aware Malware Detection.

[BibT_eX]

[DOI]

Proceedings of the 2005 IEEE Symposium on Security and Privacy (S&P 2005), 2005

Automatic discovery of API-level exploits.

[BibT_eX]

[DOI]

Proceedings of the 27th International Conference on Software Engineering (ICSE 2005), 2005

Decision Procedures Customized for Formal Verification.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2005

Modeling and Verifying Circuits Using Generalized Relative Timing.

[BibT_eX]

[DOI]

Kenneth S. Stevens

Proceedings of the 11th International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 2005), 2005

2004

The UCLID Decision Procedure.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Abstraction-Based Satisfiability Solving of Presburger Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

A hybrid SAT-based decision procedure for separation logic with uninterpreted functions.

[BibT_eX]

[DOI]

Proceedings of the 40th Design Automation Conference, 2003

Convergence Testing in Term-Level Bounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2003

Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002

Modeling and Verification of Out-of-Order Microprocessors in UCLID.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

Deciding Separation Formulas with SAT.

[BibT_eX]

[DOI]

Ofer Strichman

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

A Modular Checker for Multithreaded Programs.

[BibT_eX]

[DOI]

Cormac Flanagan

Shaz Qadeer

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.

[BibT_eX]

[DOI]