Mahesh Viswanathan

Andreas Pavlogiannis

Proc. ACM Program. Lang., 2021

Proof Blocks: Autogradeable Scaffolding Activities for Learning to Write Proofs.

[BibT_eX]

[DOI]

CoRR, 2021

Checking LTL[F, G, X] on compressed traces in polynomial time.

[BibT_eX]

[DOI]

Minjian Zhang

Proceedings of the ESEC/FSE '21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2021

On Linear Time Decidability of Differential Privacy for Programs with Unbounded Inputs.

[BibT_eX]

[DOI]

Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

2020

Deciding memory safety for single-pass heap-manipulating programs.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

Exact quantitative probabilistic model checking through rational search.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2020

What's Decidable About Program Verification Modulo Axioms?

[BibT_eX]

[DOI]

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

Deciding Differential Privacy for Programs with Finite Inputs and Outputs.

[BibT_eX]

[DOI]

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

The Complexity of Dynamic Data Race Prediction.

[BibT_eX]

[DOI]

Andreas Pavlogiannis

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning.

[BibT_eX]

[DOI]

Proceedings of the 59th IEEE Conference on Decision and Control, 2020

STMC: Statistical Model Checker with Stratified and Antithetic Sampling.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

Decidable Synthesis of Programs with Uninterpreted Functions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

Modelchecking Safety Properties in Randomized Security Protocols.

[BibT_eX]

[DOI]

Matthew S. Bauer

Proceedings of the Logic, 2020

Atomicity Checking in Linear Time using Vector Clocks.

[BibT_eX]

[DOI]

Proceedings of the ASPLOS '20: Architectural Support for Programming Languages and Operating Systems, 2020

2019

Decidable verification of uninterpreted programs.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

Decidable and expressive classes of probabilistic automata.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 2019

Statistical verification of PCTL using antithetic and stratified samples.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2019

Automated Methods for Checking Differential Privacy.

[BibT_eX]

[DOI]

CoRR, 2019

Deciding Memory Safety for Forest Datastructures.

[BibT_eX]

[DOI]

CoRR, 2019

A Retrospective Look at the Monitoring and Checking (MaC) Framework.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 19th International Conference, 2019

2018

What happens-after the first race? enhancing the predictive power of happens-before based dynamic race detection.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

Revisiting MITL to Fix Decision Procedures.

[BibT_eX]

[DOI]

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

Data race detection on compressed traces.

[BibT_eX]

[DOI]

Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2018

A Decidable Fragment of Second Order Logic With Applications to Synthesis.

[BibT_eX]

[DOI]

Proceedings of the 27th EACSL Annual Conference on Computer Science Logic, 2018

Approximating Probabilistic Automata by Regular Languages.

[BibT_eX]

[DOI]

Proceedings of the 27th EACSL Annual Conference on Computer Science Logic, 2018

Relating Syntactic and Semantic Perturbations of Hybrid Automata.

[BibT_eX]

[DOI]

Proceedings of the 29th International Conference on Concurrency Theory, 2018

Controller Synthesis Made Real: Reach-Avoid Specifications and Linear Dynamics.

[BibT_eX]

[DOI]

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

Model Checking Indistinguishability of Randomized Security Protocols.

[BibT_eX]

[DOI]

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

Statistical Verification of PCTL Using Stratified Samples.

[BibT_eX]

[DOI]

Proceedings of the 6th IFAC Conference on Analysis and Design of Hybrid Systems, 2018

2017

Stability Analysis of Switched Linear Systems Defined by Regular Languages.

[BibT_eX]

[DOI]

IEEE Trans. Autom. Control., 2017

HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata.

[BibT_eX]

[DOI]

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

Optimal Translation of LTL to Limit Deterministic Automata.

[BibT_eX]

[DOI]

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

Extending Parikh's Theorem to Weighted and Probabilistic Context-Free Grammars.

[BibT_eX]

[DOI]

Vijay Bhattiprolu

Spencer Gordon

Proceedings of the Quantitative Evaluation of Systems - 14th International Conference, 2017

Dynamic race prediction in linear time.

[BibT_eX]

[DOI]

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

Verification of randomized security protocols.

[BibT_eX]

[DOI]

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Statistical Verification of the Toyota Powertrain Control Verification Benchmark.

[BibT_eX]

[DOI]

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

Robust Model Checking of Timed Automata under Clock Drifts.

[BibT_eX]

[DOI]

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

Complexity of Model Checking MDPs against LTL Specifications.

[BibT_eX]

[DOI]

Proceedings of the 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2017

Emptiness Under Isolation and the Value Problem for Hierarchical Probabilistic Automata.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2017

Modular Verification of Protocol Equivalence in the Presence of Randomness.

[BibT_eX]

[DOI]

Matthew S. Bauer

Proceedings of the Computer Security - ESORICS 2017, 2017

DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems.

[BibT_eX]

[DOI]

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

2016

Hybridization Based CEGAR for Hybrid Automata with Affine Dynamics.

[BibT_eX]

[DOI]

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

Composing Protocols with Randomized Actions.

[BibT_eX]

[DOI]

Matthew S. Bauer

Proceedings of the Principles of Security and Trust - 5th International Conference, 2016

Verifying Continuous-time Stochastic Hybrid Systems via Mori-Zwanzig model reduction.

[BibT_eX]

[DOI]

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

Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Parsimonious, Simulation Based Verification of Linear Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP.

[BibT_eX]

[DOI]

Proceedings of the 2016 IEEE Conference on Control Applications, 2016

2015

How Can Automatic Feedback Help Students Construct Automata?

[BibT_eX]

[DOI]

ACM Trans. Comput. Hum. Interact., 2015

A decidable class of planar linear hybrid systems.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2015

Stability Preserving Simulations and Bisimulations for Hybrid Systems.

[BibT_eX]

[DOI]

IEEE Trans. Autom. Control., 2015

Statistical model checking for unbounded until formulas.

[BibT_eX]

[DOI]

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

Statistical model checking: challenges and perspectives.

[BibT_eX]

[DOI]

Axel Legay

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

Hybrid automata-based CEGAR for rectangular hybrid systems.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2015

Limit Deterministic and Probabilistic Automata for LTL ∖ GU.

[BibT_eX]

[DOI]

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

C2E2: A Verification Tool for Stateflow Models.

[BibT_eX]

[DOI]

Matthew Potok

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

Analyzing Real Time Linear Control Systems Using Software Verification.

[BibT_eX]

[DOI]

Proceedings of the 2015 IEEE Real-Time Systems Symposium, 2015

Statistical verification of dynamical systems using set oriented methods.

[BibT_eX]

[DOI]

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

C2E2: a tool for verifying annotated hybrid systems.

[BibT_eX]

[DOI]

Matthew Potok

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

Deciding Concurrent Planar Monotonic Linear Hybrid Systems.

[BibT_eX]

[DOI]

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

Floating Time Transition System: More Efficient Analysis of Timed Actors.

[BibT_eX]

[DOI]

Proceedings of the Formal Aspects of Component Software - 12th International Conference, 2015

Progress on Powertrain Verification Challenge with C2E2.

[BibT_eX]

[DOI]

Chuchu Fan

Proceedings of the 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems, 2015

Meeting a Powertrain Verification Challenge.

[BibT_eX]

[DOI]

Chuchu Fan

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

A Mori-Zwanzig and MITL Based Approach to Statistical Verification of Continuous-time Dynamical Systems.

[BibT_eX]

[DOI]

Proceedings of the 5th IFAC Conference on Analysis and Design of Hybrid Systems, 2015

2014

Least upper bounds for probability measures and their applications to abstractions.

[BibT_eX]

[DOI]

Ramesh Viswanathan

Inf. Comput., 2014

Probabilistic Automata for Safety LTL Specifications.

[BibT_eX]

[DOI]

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

Decidable Problems for Unary PFAs.

[BibT_eX]

[DOI]

Proceedings of the Quantitative Evaluation of Systems - 11th International Conference, 2014

Quantitative Information Flow in Boolean Programs.

[BibT_eX]

[DOI]

Proceedings of the Principles of Security and Trust - Third International Conference, 2014

Time-Bounded Reachability for Initialized Hybrid Automata with Linear Differential Inclusions and Rectangular Constraints.

[BibT_eX]

[DOI]

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

Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol.

[BibT_eX]

[DOI]

Proceedings of the FM 2014: Formal Methods, 2014

Stability of linear autonomous systems under regular switching sequences.

[BibT_eX]

[DOI]

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

2013

Reachability under Contextual Locking.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2013

Probabilistic Automata with Isolated Cut-Points.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2013, 2013

Automated Grading of DFA Constructions.

[BibT_eX]

[DOI]

Proceedings of the IJCAI 2013, 2013

On the decidability of stability of hybrid systems.

[BibT_eX]

[DOI]

Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013

Verification of annotated models from executions.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Embedded Software, 2013

2012

Verification of Bounded Discrete Horizon Hybrid Automata.

[BibT_eX]

[DOI]

IEEE Trans. Autom. Control., 2012

Reachability under Contextual Locking.

[BibT_eX]

[DOI]

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

Pre-orders for reasoning about stability.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control (part of CPS Week 2012), 2012

Conformance Testing of Boolean Programs with Multiple Faults.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Systems, 2012

2011

Specifications for decidable hybrid games.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2011

Power of Randomization in Automata on Infinite Strings

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2011

Probabilistic Büchi Automata with Non-extremal Acceptance Thresholds.

[BibT_eX]

[DOI]

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

Model Checking MDPs with a Unique Compact Invariant Set of Distributions.

[BibT_eX]

[DOI]

Vijay Anand Korthikanti

YoungMin Kwon

Proceedings of the Eighth International Conference on Quantitative Evaluation of Systems, 2011

A dynamic algorithm for approximate flow computations.

[BibT_eX]

[DOI]

Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, 2011

2010

A counterexample-guided abstraction-refinement framework for markov decision processes.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2010

Assertion Checking in J-Sim Simulation Models of Network Protocols.

[BibT_eX]

[DOI]

Simul., 2010

Complexity Bounds for the Verification of Real-Time Software.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2010

Reasoning about MDPs as Transformers of Probability Distributions.

[BibT_eX]

[DOI]

Vijay Anand Korthikanti

YoungMin Kwon

Proceedings of the QEST 2010, 2010

Model Checking Concurrent Programs with Nondeterminism and Randomization.

[BibT_eX]

[DOI]

Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2010

2009

Deciding branching time properties for asynchronous programs.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2009

On the expressiveness and complexity of randomization in finite state monitors.

[BibT_eX]

[DOI]

J. ACM, 2009

Verifying Tolerant Systems Using Polynomial Approximations.

[BibT_eX]

[DOI]

Proceedings of the 30th IEEE Real-Time Systems Symposium, 2009

Simulation + Hypothesis Testing for Model Checking of Probabilistic Systems.

[BibT_eX]

[DOI]

Axel Legay

Proceedings of the QEST 2009, 2009

Query Automata for Nested Words.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2009, 2009

STORMED Hybrid Games.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 12th International Conference, 2009

On Convergence of Concurrent Systems under Regular Interactions.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2009 - Concurrency Theory, 20th International Conference, 2009

2008

Incremental state-space exploration for programs with dynamically allocated data.

[BibT_eX]

[DOI]

Proceedings of the 30th International Conference on Software Engineering (ICSE 2008), 2008

STORMED Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 35th International Colloquium, 2008

Modular Preservation of Safety Properties by Cookie-Based DoS-Protection Wrappers.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2008

2007

Learning to verify branching time properties.

[BibT_eX]

[DOI]

Abhay Vardhan

Formal Methods Syst. Des., 2007

Visibly pushdown automata for streaming XML.

[BibT_eX]

[DOI]

Proceedings of the 16th International Conference on World Wide Web, 2007

J-Sim: An Integrated Environment for Simulation and Model Checking of Network Protocols.

[BibT_eX]

[DOI]

Proceedings of the 21th International Parallel and Distributed Processing Symposium (IPDPS 2007), 2007

Decidability Results for Well-Structured Transition Systems with Auxiliary Storage.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2007 - Concurrency Theory, 18th International Conference, 2007

2006

Model-Checking Markov Chains in the Presence of Uncertainties.

[BibT_eX]

[DOI]

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

Propositional Tree Automata.

[BibT_eX]

[DOI]

Joe Hendrix

Hitoshi Ohsaki

Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

Minimization, Learning, and Conformance Testing of Boolean Programs.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2006 - Concurrency Theory, 17th International Conference, 2006

LEVER: A Tool for Learning Based Verification.

[BibT_eX]

[DOI]

Abhay Vardhan

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Model Checking Multithreaded Programs with Asynchronous Atomic Methods.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

On the Complexity of Error Explanation.

[BibT_eX]

[DOI]

Nirman Kumar

Proceedings of the Verification, 2005

Using Language Inference to Verify Omega-Regular Properties.

[BibT_eX]

[DOI]

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

Conformance testing in the presence of multiple faults.

[BibT_eX]

[DOI]

Proceedings of the Sixteenth Annual ACM-SIAM Symposium on Discrete Algorithms, 2005

VESTA: A Statistical Model-checker and Analyzer for Probabilistic Systems.

[BibT_eX]

[DOI]

Gul A. Agha

Proceedings of the Second International Conference on the Quantitative Evaluaiton of Systems (QEST 2005), 2005

Finding Bugs in Network Protocols Using Simulation Code and Protocol-Specific Heuristics.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2005

Congruences for Visibly Pushdown Languages.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 32nd International Colloquium, 2005

On Statistical Model Checking of Stochastic Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004

Java-MaC: A Run-Time Assurance Approach for Java Programs.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2004

Learning Continuous Time Markov Chains from Sample Executions.

[BibT_eX]

[DOI]

Proceedings of the 1st International Conference on Quantitative Evaluation of Systems (QEST 2004), 2004

Check and simulate: a case for incorporating model checking in network simulation.

[BibT_eX]

[DOI]

Ahmed Sobeih

Jennifer C. Hou

Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 2004

Foundations for the Run-Time Monitoring of Reactive Systems - Fundamentals of the MaC Language.

[BibT_eX]

[DOI]

Moonzoo Kim

Proceedings of the Theoretical Aspects of Computing, 2004

Learning to Verify Safety Properties.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2004

Actively Learning to Verify Safety for FIFO Automata.

[BibT_eX]

[DOI]

Proceedings of the FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 2004

A Higher Order Modal Fixed Point Logic.

[BibT_eX]

[DOI]

Ramesh Viswanathan

Proceedings of the CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31, 2004

Statistical Model Checking of Black-Box Probabilistic Systems.

[BibT_eX]

[DOI]

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

2003

Preface.

[BibT_eX]

[DOI]

Oleg Sokolsky

Proceedings of the Third Workshop on Run-time Verification, 2003

Testing Extended Regular Language Membership Incrementally by Rewriting.

[BibT_eX]

[DOI]

Grigore Rosu

Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

2002

Verisim: Formal Analysis of Network Simulations.

[BibT_eX]

[DOI]

Karthikeyan Bhargavan

IEEE Trans. Software Eng., 2002

An Approximate L1-Difference Algorithm for Massive Data Streams.

[BibT_eX]

[DOI]

SIAM J. Comput., 2002

Computational Analysis of Run-time Monitoring - Fundamentals of Java-MaC.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification 2002, 2002

Testing and Spot-Checking of Data Streams.

[BibT_eX]

[DOI]

Algorithmica, 2002

2001

Java-MaC: a Run-time Assurance Tool for Java Programs.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Runtime Verification, 2001

Foundations for Circular Compositional Reasoning.

[BibT_eX]

[DOI]

Ramesh Viswanathan

Proceedings of the Automata, Languages and Programming, 28th International Colloquium, 2001

2000

Spot-Checkers.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 2000

Testing and spot-checking of data streams (extended abstract).

[BibT_eX]

[DOI]

Proceedings of the Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, 2000

The Relationship between Public Key Encryption and Oblivious Transfer.

[BibT_eX]

[DOI]

Proceedings of the 41st Annual Symposium on Foundations of Computer Science, 2000

1999

The Complexity of Problems on Graphs Represented as OBDDs.

[BibT_eX]

[DOI]

Chic. J. Theor. Comput. Sci., 1999

Steering of real-time systems based on monitoring and checking.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Workshop on Object-Oriented Real-Time Dependable Systems, 1999

Runtime Assurance Based On Formal Specifications.

[BibT_eX]

Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 1999

An Approximate L<sup>1</sup>-Difference Algorithm for Massive Data Streams.

[BibT_eX]

[DOI]

Proceedings of the 40th Annual Symposium on Foundations of Computer Science, 1999

Formally specified monitoring of temporal properties.

[BibT_eX]

[DOI]

Proceedings of the 11th Euromicro Conference on Real-Time Systems (ECRTS 1999), 1999

1998

Complexity of Problems on Graphs Represented as OBDDs (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the STACS 98, 1998

Membership Questions for Timed and Hybrid Automata.

[BibT_eX]

[DOI]

Rajeev Alur

Robert P. Kurshan