Rajeev Alur

Orcid: 0000-0003-1733-7083

Affiliations:
  • University of Pennsylvania, Philadelphia, PA, USA


According to our database1, Rajeev Alur authored at least 283 papers between 1990 and 2024.

Collaborative distances:

Awards

IEEE Fellow

IEEE Fellow 2008, "For contributions to automata, logics, and verification techniques for real-time and hybrid systems".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Logicbreaks: A Framework for Understanding Subversion of Rule-based Inference.
CoRR, 2024

Data-Efficient Learning with Neural Programs.
CoRR, 2024

Chordal sparsity for SDP-based neural network verification.
Autom., 2024

TYGR: Type Inference on Stripped Binaries using Graph Neural Networks.
Proceedings of the 33rd USENIX Security Symposium, 2024

MuCache: A General Framework for Caching in Microservice Graphs.
Proceedings of the 21st USENIX Symposium on Networked Systems Design and Implementation, 2024

Relational Programming with Foundational Models.
Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024

2023
Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates.
Proc. ACM Program. Lang., October, 2023

Executing Microservice Applications on Serverless, Correctly.
Proc. ACM Program. Lang., January, 2023

A Robust Theory of Series Parallel Graphs.
Proc. ACM Program. Lang., January, 2023

Relational Query Synthesis ⋈ Decision Tree Learning.
Proc. VLDB Endow., 2023

Regular Transformations (Dagstuhl Seminar 23202).
Dagstuhl Reports, 2023

Understanding the Effectiveness of Large Language Models in Detecting Security Vulnerabilities.
CoRR, 2023

Stability Guarantees for Feature Attributions with Multiplicative Smoothing.
Proceedings of the Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, 2023

Robust Subtask Learning for Compositional Generalization.
Proceedings of the International Conference on Machine Learning, 2023

Policy Synthesis and Reinforcement Learning for Discounted LTL.
Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022
Static detection of uncoalesced accesses in GPU programs.
Formal Methods Syst. Des., February, 2022

Composing Copyless Streaming String Transducers.
CoRR, 2022

Parametric Chordal Sparsity for SDP-based Neural Network Verification.
CoRR, 2022

Automatic Repair for Network Programs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Stream processing with dependency-guided synchronization.
Proceedings of the PPoPP '22: 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Seoul, Republic of Korea, April 2, 2022

Correctness in Stream Processing: Challenges and Opportunities.
Proceedings of the 12th Conference on Innovative Data Systems Research, 2022

Chordal Sparsity for Lipschitz Constant Estimation of Deep Neural Networks.
Proceedings of the 61st IEEE Conference on Decision and Control, 2022

Specification-Guided Learning of Nash Equilibria with High Social Welfare.
Proceedings of the Computer Aided Verification - 34th International Conference, 2022

A Framework for Transforming Specifications in Reinforcement Learning.
Proceedings of the Principles of Systems Design, 2022

2021
Compositional Learning and Verification of Neural Network Controllers.
ACM Trans. Embed. Comput. Syst., 2021

Verifying the Safety of Autonomous Systems with Neural Network Controllers.
ACM Trans. Embed. Comput. Syst., 2021

Colored nested words.
Formal Methods Syst. Des., 2021

Orion: Automatic Repair for Network Programs.
CoRR, 2021

Network Traffic Classification by Program Synthesis.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

Synchronization Schemas.
Proceedings of the PODS'21: Proceedings of the 40th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, 2021

Example-guided synthesis of relational queries.
Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

Compositional Reinforcement Learning from Logical Specifications.
Proceedings of the Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, 2021

Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Abstract Value Iteration for Hierarchical Reinforcement Learning.
Proceedings of the 24th International Conference on Artificial Intelligence and Statistics, 2021

2020
Streamable regular transductions.
Theor. Comput. Sci., 2020

DiffStream: differential output testing for stream processing programs.
Proc. ACM Program. Lang., 2020

Session-layer Attack Traffic Classification by Program Synthesis.
CoRR, 2020

Computer-Aided Personalized Education.
CoRR, 2020

REAFFIRM: Model-Based Repair of Hybrid Systems for Improving Resiliency.
Proceedings of the 18th ACM/IEEE International Conference on Formal Methods and Models for System Design, 2020

Space-efficient Query Evaluation over Probabilistic Event Streams.
Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

Case study: verifying the safety of an autonomous racing car with a neural network controller.
Proceedings of the HSCC '20: 23rd ACM International Conference on Hybrid Systems: Computation and Control, 2020

2019
Continuous-Time Models for System Design and Analysis.
Proceedings of the Computing and Software Science - State of the Art and Perspectives, 2019

Modular quantitative monitoring.
Proc. ACM Program. Lang., 2019

SyGuS-Comp 2018: Results and Analysis.
CoRR, 2019

Data-trace types for distributed stream processing systems.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

A Composable Specification Language for Reinforcement Learning Tasks.
Proceedings of the Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, 2019

Detecting security leaks in hybrid systems with information flow analysis.
Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design, 2019

Verisig: verifying safety properties of hybrid systems with neural network controllers.
Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019

2018
Model Checking Procedural Programs.
Proceedings of the Handbook of Model Checking., 2018

NetEgg: A Scenario-Based Programming Toolkit for SDN Policies.
IEEE/ACM Trans. Netw., 2018

Real-Time Decision Policies With Predictable Performance.
Proc. IEEE, 2018

Compositional and symbolic synthesis of reactive controllers for multi-agent systems.
Inf. Comput., 2018

Equilibria in Quantitative Concurrent Games.
CoRR, 2018

Search-based program synthesis.
Commun. ACM, 2018

Block-Size Independence for GPU Programs.
Proceedings of the Static Analysis - 25th International Symposium, 2018

Accelerating search-based program synthesis using learned probabilistic models.
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Quantitative Regular Expressions for Monitoring Cardiac Arrhythmias.
Proceedings of the 3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, 2018

Interfaces for Stream Processing Systems.
Proceedings of the Principles of Modeling, 2018

2017
An Introduction to the StreamQRE Language.
Proceedings of the Dependable Software Systems Engineering, 2017

Schedulability of Bounded-Rate Multimode Systems.
ACM Trans. Embed. Comput. Syst., 2017

Automatic Synthesis of Distributed Protocols.
SIGACT News, 2017

Streaming Tree Transducers.
J. ACM, 2017

SyGuS-Comp 2017: Results and Analysis.
Proceedings of the Proceedings Sixth Workshop on Synthesis, 2017

Scaling Enumerative Program Synthesis via Divide and Conquer.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Quantitative Network Monitoring with NetQRE.
Proceedings of the Conference of the ACM Special Interest Group on Data Communication, 2017

StreamQRE: modular specification and efficient evaluation of quantitative queries over streaming data.
Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

Automata-Based Stream Processing.
Proceedings of the 44th International Colloquium on Automata, Languages, and Programming, 2017

GPUDrano: Detecting Uncoalesced Accesses in GPU Programs.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Derivatives of Quantitative Regular Expressions.
Proceedings of the Models, Algorithms, Logics and Tools, 2017

2016
SyGuS-Comp 2016: Results and Analysis.
Proceedings of the Proceedings Fifth Workshop on Synthesis, 2016

Systems Computing Challenges in the Internet of Things.
CoRR, 2016

Compositional Synthesis with Parametric Reactive Controllers.
Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, 2016

Regular Programming for Quantitative Properties of Data Streams.
Proceedings of the Programming Languages and Systems, 2016

Hedging Bets in Markov Decision Processes.
Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

Compositional Synthesis of Reactive Controllers for Multi-agent Systems.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015

How Can Automatic Feedback Help Students Construct Automata?
ACM Trans. Comput. Hum. Interact., 2015

Theory in practice for system design and verification.
ACM SIGLOG News, 2015

Automata Tutor and what we learned from building an online teaching tool.
Bull. EATCS, 2015

Results and Analysis of SyGuS-Comp'15.
Proceedings of the Proceedings Fourth Workshop on Synthesis, 2015

Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

DReX: A Declarative Language for Efficiently Evaluating Regular String Transformations.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Keynote talk I: Syntax-guided synthesis.
Proceedings of the 13. ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2015

Scenario-based programming for SDN policies.
Proceedings of the 11th ACM Conference on Emerging Networking Experiments and Technologies, 2015

Automatic Completion of Distributed Protocols with Symmetry.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Synthesis Through Unification.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014
Closed-loop verification of medical devices with model abstraction and refinement.
Int. J. Softw. Tools Technol. Transf., 2014

Synthesizing Finite-State Protocols from Scenarios and Requirements.
Proceedings of the Hardware and Software: Verification and Testing, 2014

NetEgg: Programming Network Policies by Examples.
Proceedings of the 13th ACM Workshop on Hot Topics in Networks, 2014

Precise piecewise affine models from input-output data.
Proceedings of the 2014 International Conference on Embedded Software, 2014

Regular combinators for string transformations.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

Symbolic Visibly Pushdown Automata.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013
Can we verify cyber-physical systems?: technical perspective.
Commun. ACM, 2013

TRANSIT: specifying protocols with concolic snippets.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

Tutorial I: Syntax-guided synthesis.
Proceedings of the 11th ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2013

From Monadic Second-Order Definable String Transformations to Transducers.
Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Regular Functions and Cost Register Automata.
Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

On the Complexity of Shortest Path Problems on Discounted Cost Graphs.
Proceedings of the Language and Automata Theory and Applications, 2013

Automated Grading of DFA Constructions.
Proceedings of the IJCAI 2013, 2013

Decision Problems for Additive Regular Functions.
Proceedings of the Automata, Languages, and Programming - 40th International Colloquium, 2013

Safe schedulability of bounded-rate multi-mode systems.
Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013

Towards synthesis of platform-aware attack-resilient control systems: extended abstract.
Proceedings of the 2nd ACM International Conference on High Confidence Networked Systems (part of CPS Week), 2013

Transducer-Based Algorithmic Verification of Retransmission Protocols over Noisy Channels.
Proceedings of the Formal Techniques for Distributed Systems, 2013

On the feasibility of automation for bandwidth allocation problems in data centers.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

Counter-strategy guided refinement of GR(1) temporal logic specifications.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

Syntax-guided synthesis.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012
Algorithmic analysis of array-accessing programs.
ACM Trans. Comput. Log., 2012

Time-Triggered Implementations of Dynamic Controllers.
ACM Trans. Embed. Comput. Syst., 2012

2011 CAV award announcement.
Formal Methods Syst. Des., 2012

2010 CAV award announcement.
Formal Methods Syst. Des., 2012

Modeling and Verification of a Dual Chamber Implantable Pacemaker.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Regular Transformations of Infinite Strings.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Optimal scheduling for constant-rate multi-mode systems.
Proceedings of the Hybrid Systems: Computation and Control (part of CPS Week 2012), 2012

An Axiomatic Memory Model for POWER Multiprocessors.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011
Software model checking using languages of nested trees.
ACM Trans. Program. Lang. Syst., 2011

Compositional Modeling and Analysis of Multi-Hop Control Networks.
IEEE Trans. Autom. Control., 2011

Regular Functions, Cost Register Automata, and Generalized Min-Cost Problems
CoRR, 2011

Streaming String Transducers.
Proceedings of the Logic, Language, Information and Computation, 2011

Streaming transducers for algorithmic verification of single-pass list-processing programs.
Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Nondeterministic Streaming String Transducers.
Proceedings of the Automata, Languages and Programming - 38th International Colloquium, 2011

Interfaces for Control Components.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2011

Relating average and discounted costs for quantitative analysis of timed systems.
Proceedings of the 11th International Conference on Embedded Software, 2011

Formal verification of hybrid systems.
Proceedings of the 11th International Conference on Embedded Software, 2011

Litmus tests for comparing memory consistency models: how long do they need to be?
Proceedings of the 48th Design Automation Conference, 2011

2010
Active Learning of Plans for Safety and Reachability Goals With Partial Observability.
IEEE Trans. Syst. Man Cybern. Part B, 2010

Algorithmic Verification of Single-Pass List Processing Programs
CoRR, 2010

Temporal Reasoning for Procedural Programs.
Proceedings of the Verification, 2010

Representation dependence testing using program inversion.
Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010

Expressiveness of streaming string transducers.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2010

Generating Litmus Tests for Contrasting Memory Consistency Models.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Model Checking of Linearizability of Concurrent List Implementations.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009
Adding nesting structure to words.
J. ACM, 2009

Modeling and Analysis of Multi-hop Control Networks.
Proceedings of the 15th IEEE Real-Time and Embedded Technology and Applications Symposium, 2009

Specification and Analysis of Network Resource Requirements of Control Systems.
Proceedings of the Hybrid Systems: Computation and Control, 12th International Conference, 2009

On Omega-Languages Defined by Mean-Payoff Conditions.
Proceedings of the Foundations of Software Science and Computational Structures, 2009

Temporal Reasoning about Program Executions.
Proceedings of the Foundations of Software Science and Computational Structures, 2009

Robust stability of multi-hop control networks.
Proceedings of the 48th IEEE Conference on Decision and Control, 2009

Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Automated Analysis of Java Methods for Confidentiality.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Scalable scheduling algorithms for wireless networked control systems.
Proceedings of the IEEE Conference on Automation Science and Engineering, 2009

2008
First-Order and Temporal Logics for Nested Words.
Log. Methods Comput. Sci., 2008

Automatic symbolic compositional verification by learning assumptions.
Formal Methods Syst. Des., 2008

Introduction.
Formal Methods Syst. Des., 2008

Model Checking: From Tools to Theory.
Proceedings of the 25 Years of Model Checking - History, Achievements, Perspectives, 2008

Regular Specifications of Resource Requirements for Embedded Control Software.
Proceedings of the 14th IEEE Real-Time and Embedded Technology and Applications Symposium, 2008

RTComposer: a framework for real-time components with scheduling interfaces.
Proceedings of the 8th ACM & IEEE International conference on Embedded software, 2008

Symbolic analysis for improving simulation coverage of Simulink/Stateflow models.
Proceedings of the 8th ACM & IEEE International conference on Embedded software, 2008

Ranking Automata and Games for Prioritized Requirements.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Marrying Words and Trees.
Proceedings of the Algebraic Methodology and Software Technology, 2008

2007
Dispatch sequences for embedded control models.
J. Comput. Syst. Sci., 2007

Model Checking on Trees with Path Equivalences.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Instrumenting C Programs with Nested Word Monitors.
Proceedings of the Model Checking Software, 2007

CheckFence: checking consistency of concurrent data types on relaxed memory models.
Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Automata Based Interfaces for Control and Scheduling.
Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007

Symbolic Analysis for GSMP Models with One Stateful Clock.
Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007

2006
Predicate abstraction for reachability analysis of hybrid systems.
ACM Trans. Embed. Comput. Syst., 2006

Modular strategies for recursive game graphs.
Theor. Comput. Sci., 2006

Counterexample-guided predicate abstraction of hybrid systems.
Theor. Comput. Sci., 2006

Compositional modeling and refinement for hierarchical hybrid systems.
J. Log. Algebraic Methods Program., 2006

A fixpoint calculus for local and global program flows.
Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

Preserving Secrecy Under Refinement.
Proceedings of the Automata, Languages and Programming, 33rd International Colloquium, 2006

Bounded Model Checking for GSMP Models of Stochastic Real-Time Systems.
Proceedings of the Hybrid Systems: Computation and Control, 9th International Workshop, 2006

Branching Pushdown Tree Automata.
Proceedings of the FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 2006

Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Languages of Nested Trees.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition.
Proceedings of the Automated Technology for Verification and Analysis, 2006

2005
Analysis of recursive state machines.
ACM Trans. Program. Lang. Syst., 2005

Preface.
ACM Trans. Embed. Comput. Syst., 2005

Realizability and verification of MSC graphs.
Theor. Comput. Sci., 2005

Symbolic computational techniques for solving games.
Int. J. Softw. Tools Technol. Transf., 2005

Deciding Global Partial-Order Properties.
Formal Methods Syst. Des., 2005

Trends and Challenges in Algorithmic Software Verification.
Proceedings of the Verified Software: Theories, 2005

Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement.
Proceedings of the Verification, 2005

On-the-Fly Reachability and Cycle Detection for Recursive State Machines.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Quantifying the Gap between Embedded Control Models and Time-Triggered Implementations.
Proceedings of the 26th IEEE Real-Time Systems Symposium (RTSS 2005), 2005

Synthesis of interface specifications for Java classes.
Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

Congruences for Visibly Pushdown Languages.
Proceedings of the Automata, Languages and Programming, 32nd International Colloquium, 2005

Perturbed Timed Automata.
Proceedings of the Hybrid Systems: Computation and Control, 8th International Workshop, 2005

The Benefits of Exposing Calls and Returns.
Proceedings of the CONCUR 2005 - Concurrency Theory, 16th International Conference, 2005

Symbolic Compositional Verification by Learning Assumptions.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004
Modular refinement of hierarchic reactive machines.
ACM Trans. Program. Lang. Syst., 2004

Deterministic generators and games for Ltl fragments.
ACM Trans. Comput. Log., 2004

Optimal paths in weighted timed automata.
Theor. Comput. Sci., 2004

Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System.
Int. J. Softw. Tools Technol. Transf., 2004

Polyhedral Flows in Hybrid Automata.
Formal Methods Syst. Des., 2004

A Temporal Logic of Nested Calls and Returns.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Visibly pushdown languages.
Proceedings of the 36th Annual ACM Symposium on Theory of Computing, 2004

Decision Problems for Timed Automata: A Survey.
Proceedings of the Formal Methods for the Design of Real-Time Systems, 2004

Optimal Reachability for Weighted Timed Games.
Proceedings of the Automata, Languages and Programming: 31st International Colloquium, 2004

Structured Modeling of Concurrent Stochastic Hybrid Systems.
Proceedings of the Formal Techniques, 2004

Variable Reuse for Efficient Image Computation.
Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

A model-based approach to integrating security policies for embedded devices.
Proceedings of the EMSOFT 2004, 2004

Games for Formal Design and Verification of Reactive Systems.
Proceedings of the Automated Technology for Verification and Analysis: Second International Conference, 2004

2003
Inference of Message Sequence Charts.
IEEE Trans. Software Eng., 2003

Hierarchical modeling and analysis of embedded systems.
Proc. IEEE, 2003

Counter-Example Guided Predicate Abstraction of Hybrid Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

Generating embedded software from hierarchical hybrid models.
Proceedings of the 2003 Conference on Languages, 2003

Progress on Reachability Analysis of Hybrid Systems Using Predicate Abstraction.
Proceedings of the Hybrid Systems: Computation and Control, 2003

Playing Games with Boxes and Diamonds.
Proceedings of the CONCUR 2003, 2003

Compression of Partially Ordered Strings.
Proceedings of the CONCUR 2003, 2003

Modular Strategies for Infinite Games on Recursive Graphs.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

Formal Analysis of Hierarchical State Machines.
Proceedings of the Verification: Theory and Practice, 2003

2002
Alternating-time temporal logic.
J. ACM, 2002

A Framework and Architecture for Multi-Robot Coordination.
Int. J. Robotics Res., 2002

Modeling and analyzing biomolecular networks.
Comput. Sci. Eng., 2002

Reachability Analysis of Hybrid Systems via Predicate Abstraction.
Proceedings of the Hybrid Systems: Computation and Control, 5th International Workshop, 2002

Visual Programming for Modeling and Simulation of Biomolecular Regulatory Networks.
Proceedings of the High Performance Computing, 2002

Exploiting Behavioral Hierarchy for Efficient Model Checking.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

Predictable programs in barcodes.
Proceedings of the International Conference on Compilers, 2002

2001
Model checking of hierarchical state machines.
ACM Trans. Program. Lang. Syst., 2001

Parametric temporal logic for "model measuring".
ACM Trans. Comput. Log., 2001

Partial-Order Reduction in Symbolic State-Space Exploration.
Formal Methods Syst. Des., 2001

Shared Variables Interaction Diagrams.
Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 2001

JMOCHA: A Model Checking Tool that Exploits Design Structure.
Proceedings of the 23rd International Conference on Software Engineering, 2001

Compositional Refinement for Hierarchical Hybrid Systems.
Proceedings of the Hybrid Systems: Computation and Control, 4th International Workshop, 2001

Hybrid Modeling and Simulation of Biomolecular Networks.
Proceedings of the Hybrid Systems: Computation and Control, 4th International Workshop, 2001

Hierarchical Hybrid Modeling of Embedded Systems.
Proceedings of the Embedded Software, First International Workshop, 2001

Heuristics for Hierarchical Partitioning with Application to Model Checking.
Proceedings of the Correct Hardware Design and Verification Methods, 2001

Verifying Network Protocol Implementations by Symbolic Refinement Checking.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001

Analysis of Recursive State Machines.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000
Computer-aided verification of reactive systems.
ACM SIGSOFT Softw. Eng. Notes, 2000

Discrete abstractions of hybrid systems.
Proc. IEEE, 2000

Model-Checking of Correctness Conditions for Concurrent Objects.
Inf. Comput., 2000

A Framework and Architecture for Multirobot Coordination.
Proceedings of the Experimental Robotics VII [ISER 2000, 2000

Modular Specification of Hybrid Systems in CHARON.
Proceedings of the Hybrid Systems: Computation and Control, Third International Workshop, 2000

Automated Refinement Checking for Asynchronous Processes.
Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

Exploiting Hierarchical Structure for Efficient Formal Verification.
Proceedings of the CONCUR 2000, 2000

Efficient Reachability Analysis of Hierarchical Reactive Machines.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999
Event-Clock Automata: A Determinizable Class of Timed Automata.
Theor. Comput. Sci., 1999

Undecidability of Partial Order Logics.
Inf. Process. Lett., 1999

Reactive Modules.
Formal Methods Syst. Des., 1999

Introduction.
Formal Methods Syst. Des., 1999

Communicating Hierarchical State Machines.
Proceedings of the Automata, 1999

Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination.
Proceedings of the FM'99 - Formal Methods, 1999

Model Checking of Message Sequence Charts.
Proceedings of the CONCUR '99: Concurrency Theory, 1999

"Next" Heuristic for On-the-Fly Model Checking.
Proceedings of the CONCUR '99: Concurrency Theory, 1999

Automating Modular Verification.
Proceedings of the CONCUR '99: Concurrency Theory, 1999

Timed Automata.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998
Finitary Fairness.
ACM Trans. Program. Lang. Syst., 1998

Symbolic Exploration of transition Hierarchies.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998

Membership Questions for Timed and Hybrid Automata.
Proceedings of the 19th IEEE Real-Time Systems Symposium, 1998

Efficient Formal Verification of Hierarchical Descriptions.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1998

Performance Evaluation and Prediction.
Proceedings of the Euro-Par '98 Parallel Processing, 1998

Alternating Refinement Relations.
Proceedings of the CONCUR '98: Concurrency Theory, 1998

MOCHA: Modularity in Model Checking.
Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997
Real-Time System = Discrete System + Clock Variables.
Int. J. Softw. Tools Technol. Transf., 1997

Time-Adaptive Algorithms for Synchronization.
SIAM J. Comput., 1997

Computing Accumulated Delays in Real-time Systems.
Formal Methods Syst. Des., 1997

Model-Checking of Real-Time Systems: A Telecommunications Application (Experience Report).
Proceedings of the Pulling Together, 1997

Modularity for Timed and Hybrid Systems.
Proceedings of the CONCUR '97: Concurrency Theory, 1997

1996
Automatic Symbolic Verification of Embedded Systems.
IEEE Trans. Software Eng., 1996

An Analyzer for Message Sequence Charts.
Softw. Concepts Tools, 1996

The Benefits of Relaxing Punctuality.
J. ACM, 1996

Contention-Free Complexity of Shared Memory Algorithms.
Inf. Comput., 1996

Fast Timing-Based Algorithms.
Distributed Comput., 1996

Next Steps in Formal Verification.
ACM Comput. Surv., 1996

An Analyser for Mesage Sequence Charts.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1996

Verifying Abstractions of Timed Systems.
Proceedings of the CONCUR '96, 1996

1995
Timing Verification by Successive Approximation
Inf. Comput., April, 1995

The Algorithmic Analysis of Hybrid Systems.
Theor. Comput. Sci., 1995

Distinguishing tests for nondeterministic and probabilistic machines.
Proceedings of the Twenty-Seventh Annual ACM Symposium on Theory of Computing, 1995

Model-Checking of Causality Properties
Proceedings of the Proceedings, 1995

Timing Analysis in COSPAN.
Proceedings of the Hybrid Systems III: Verification and Control, 1995

Local Liveness for Compositional Modeling of Fair Reactive Systems.
Proceedings of the Computer Aided Verification, 1995

1994
A Theory of Timed Automata.
Theor. Comput. Sci., 1994

A Really Temporal Logic.
J. ACM, 1994

The Observational Power of Clocks.
Proceedings of the CONCUR '94, 1994

A Determinizable Class of Timed Automata.
Proceedings of the Computer Aided Verification, 6th International Conference, 1994

1993
Real-Time Logics: Complexity and Expressiveness
Inf. Comput., May, 1993

Model-Checking in Dense Real-time
Inf. Comput., May, 1993

Parametric real-time reasoning.
Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, 1993

How to Share an Object: A Fast Timing-Based Solution.
Proceedings of the Fifth IEEE Symposium on Parallel and Distributed Processing, 1993

1992
Results about Fast Mutual Exclusion.
Proceedings of the Real-Time Systems Symposium, 1992

An implementation of three algorithms for timing verification based on automata emptiness.
Proceedings of the Real-Time Systems Symposium, 1992

Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems.
Proceedings of the Hybrid Systems, 1992

Back to the Future: Towards a Theory of Timed Regular Languages
Proceedings of the 33rd Annual Symposium on Foundations of Computer Science, 1992

Minimization of Timed Transition Systems.
Proceedings of the CONCUR '92, 1992

1991
Techniques for automatic verification of real-time systems.
PhD thesis, 1991

Logics and Models of Real Time: A Survey.
Proceedings of the Real-Time: Theory in Practice, 1991

Verifying Automata Specifications of Probabilistic Real-time Systems.
Proceedings of the Real-Time: Theory in Practice, 1991

Model-Checking for Probabilistic Real-Time Systems (Extended Abstract).
Proceedings of the Automata, Languages and Programming, 18th International Colloquium, 1991

1990
Model-Checking for Real-Time Systems
Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), 1990

Automata For Modeling Real-Time Systems.
Proceedings of the Automata, Languages and Programming, 17th International Colloquium, 1990


  Loading...