| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Orna Grumberg, Moshe Y. Vardi, Joseph Sifakis, Rajeev Alur |
2010 CAV award announcement.  |
Formal Methods in System Design  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, Rahul Mangharam |
Modeling and Verification of a Dual Chamber Implantable Pacemaker. |
TACAS |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Ashutosh Trivedi, Dominik Wojtczak |
Optimal scheduling for constant-rate multi-mode systems. |
HSCC |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Alessandro D'Innocenzo, Karl Henrik Johansson, George J. Pappas, Gera Weiss |
Compositional Modeling and Analysis of Multi-Hop Control Networks. |
IEEE Trans. Automat. Contr. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Swarat Chaudhuri, P. Madhusudan |
Software model checking using languages of nested trees. |
ACM Trans. Program. Lang. Syst. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Loris D'Antoni, Jyotirmoy V. Deshmukh, Mukund Raghothaman, Yifei Yuan |
Regular Functions, Cost Register Automata, and Generalized Min-Cost Problems |
CoRR |
2011 |
DBLP BibTeX RDF |
|
| 1 | Rajeev Alur, Loris D'Antoni |
Streaming Tree Transducers |
CoRR |
2011 |
DBLP BibTeX RDF |
|
| 1 | Rajeev Alur |
Streaming String Transducers. |
WoLLIC |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Ashutosh Trivedi |
Relating average and discounted costs for quantitative analysis of timed systems. |
EMSOFT |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur |
Formal verification of hybrid systems. |
EMSOFT |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Jyotirmoy V. Deshmukh |
Nondeterministic Streaming String Transducers. |
ICALP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur |
Interfaces for Control Components. |
FORMATS |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Pavol Cerný |
Streaming transducers for algorithmic verification of single-pass list-processing programs. |
POPL |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Sela Mador-Haim, Rajeev Alur, Milo M. K. Martin |
Litmus tests for comparing memory consistency models: how long do they need to be? |
DAC |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Pavol Cerný |
Algorithmic Verification of Single-Pass List Processing Programs |
CoRR |
2010 |
DBLP BibTeX RDF |
|
| 1 | Wonhong Nam, Rajeev Alur |
Active Learning of Plans for Safety and Reachability Goals With Partial Observability. |
IEEE Transactions on Systems, Man, and Cybernetics, Part B |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Pavol Cerný, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, Rajeev Alur |
Model Checking of Linearizability of Concurrent List Implementations. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Sela Mador-Haim, Rajeev Alur, Milo M. K. Martin |
Generating Litmus Tests for Contrasting Memory Consistency Models. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Swarat Chaudhuri |
Temporal Reasoning for Procedural Programs. |
VMCAI |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Aditya Kanade, Rajeev Alur, Sriram K. Rajamani, Ganesan Ramalingam |
Representation dependence testing using program inversion. |
SIGSOFT FSE |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Pavol Cerný |
Expressiveness of streaming string transducers. |
FSTTCS |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, P. Madhusudan |
Adding nesting structure to words. |
J. ACM |
2009 |
DBLP DOI BibTeX RDF |
software model checking, tree automata, Pushdown automata, XML processing |
| 1 | Gera Weiss, Alessandro D'Innocenzo, Rajeev Alur, Karl Henrik Johansson, George J. Pappas |
Robust stability of multi-hop control networks. |
CDC |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro D'Innocenzo, Gera Weiss, Rajeev Alur, Alf J. Isaksson, Karl Henrik Johansson, George J. Pappas |
Scalable scheduling algorithms for wireless networked control systems. |
CASE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Pavol Cerný, Rajeev Alur |
Automated Analysis of Java Methods for Confidentiality. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Aditya Kanade, Rajeev Alur, Franjo Ivancic, S. Ramesh, Sriram Sankaranarayanan, K. C. Shashidhar |
Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Gera Weiss, Sebastian Fischmeister, Madhukar Anand, Rajeev Alur |
Specification and Analysis of Network Resource Requirements of Control Systems. |
HSCC |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Pavol Cerný, Scott Weinstein |
Algorithmic Analysis of Array-Accessing Programs. |
CSL |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Alessandro D'Innocenzo, Karl Henrik Johansson, George J. Pappas, Gera Weiss |
Modeling and Analysis of Multi-hop Control Networks. |
IEEE Real-Time and Embedded Technology and Applications Symposium |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur |
Temporal Reasoning about Program Executions. |
FOSSACS |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Aldric Degorre, Oded Maler, Gera Weiss |
On Omega-Languages Defined by Mean-Payoff Conditions. |
FOSSACS |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Marcelo Arenas, Pablo Barceló, Kousha Etessami, Neil Immerman, Leonid Libkin |
First-Order and Temporal Logics for Nested Words. |
Logical Methods in Computer Science |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Marcelo Arenas, Pablo Barceló, Kousha Etessami, Neil Immerman, Leonid Libkin |
First-Order and Temporal Logics for Nested Words |
CoRR |
2008 |
DBLP BibTeX RDF |
|
| 1 | Rajeev Alur, George J. Pappas |
Introduction. |
Formal Methods in System Design |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Wonhong Nam, P. Madhusudan, Rajeev Alur |
Automatic symbolic compositional verification by learning assumptions. |
Formal Methods in System Design |
2008 |
DBLP DOI BibTeX RDF |
Regular language learning, Formal verification, Symbolic model checking, Compositional verification, Assume-guarantee reasoning, Hypergraph partitioning |
| 1 | Rajeev Alur, Aditya Kanade, S. Ramesh, K. C. Shashidhar |
Symbolic analysis for improving simulation coverage of Simulink/Stateflow models. |
EMSOFT |
2008 |
DBLP DOI BibTeX RDF |
simulations, coverage, hybrid systems, Simulink, Stateflow |
| 1 | Rajeev Alur, Gera Weiss |
RTComposer: a framework for real-time components with scheduling interfaces. |
EMSOFT |
2008 |
DBLP DOI BibTeX RDF |
automata based scheduling, real time specification for java (RTSJ) |
| 1 | Rajeev Alur |
Marrying Words and Trees. |
AMAST |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur |
Model Checking: From Tools to Theory. |
25 Years of Model Checking |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Aditya Kanade, Gera Weiss |
Ranking Automata and Games for Prioritized Requirements. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Gera Weiss |
Regular Specifications of Resource Requirements for Embedded Control Software. |
IEEE Real-Time and Embedded Technology and Applications Symposium |
2008 |
DBLP DOI BibTeX RDF |
Sheduling, omega-regular, LQG, resource allocation, control, embedded, specification language, automata, exponential stability |
| 1 | Rajeev Alur, Arun Chandrashekharapuram |
Dispatch sequences for embedded control models. |
J. Comput. Syst. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur |
Marrying Words and Trees. |
CSR |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin |
CheckFence: checking consistency of concurrent data types on relaxed memory models. |
PLDI |
2007 |
DBLP DOI BibTeX RDF |
lock-free synchronization, shared-memory multiprocessors, multi-threading, software model checking, memory models, sequential consistency, concurrent data structures |
| 1 | Rajeev Alur, Pavol Cerný, Swarat Chaudhuri |
Model Checking on Trees with Path Equivalences. |
TACAS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Swarat Chaudhuri, Rajeev Alur |
Instrumenting C Programs with Nested Word Monitors. |
SPIN |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Mikhail Bernadsky, Rajeev Alur |
Symbolic Analysis for GSMP Models with One Stateful Clock. |
HSCC |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Gera Weiss, Rajeev Alur |
Automata Based Interfaces for Control and Scheduling. |
HSCC |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Marcelo Arenas, Pablo Barceló, Kousha Etessami, Neil Immerman, Leonid Libkin |
First-Order and Temporal Logics for Nested Words. |
LICS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur |
Marrying words and trees. |
PODS |
2007 |
DBLP DOI BibTeX RDF |
nested words, XML, query languages, tree automata, pushdown automata |
| 1 | Rajeev Alur, Thao Dang, Franjo Ivancic |
Predicate abstraction for reachability analysis of hybrid systems. |
ACM Trans. Embedded Comput. Syst. |
2006 |
DBLP DOI BibTeX RDF |
hybrid systems, Reachability analysis, predicate abstraction |
| 1 | Rajeev Alur, Radu Grosu, Insup Lee, Oleg Sokolsky |
Compositional modeling and refinement for hierarchical hybrid systems. |
J. Log. Algebr. Program. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Thao Dang, Franjo Ivancic |
Counterexample-guided predicate abstraction of hybrid systems. |
Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Salvatore La Torre, P. Madhusudan |
Modular strategies for recursive game graphs. |
Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur |
Games for formal design and verification of reactive systems. |
MEMOCODE |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Truong Nghiem, George J. Pappas, Rajeev Alur, Antoine Girard |
Time-triggered implementations of dynamic controllers. |
EMSOFT |
2006 |
DBLP DOI BibTeX RDF |
PI, performance, control, implementation, time-triggered, PID, dynamic controller |
| 1 | Rajeev Alur, Pavol Cerný, Steve Zdancewic |
Preserving Secrecy Under Refinement. |
ICALP |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Swarat Chaudhuri, P. Madhusudan |
A fixpoint calculus for local and global program flows. |
POPL |
2006 |
DBLP DOI BibTeX RDF |
infinite-state, model-checking, verification, games, specification, logic, ?-calculus, pushdown systems |
| 1 | Wonhong Nam, Rajeev Alur |
Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition. |
ATVA |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, P. Madhusudan |
Adding Nesting Structure to Words. |
Developments in Language Theory |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Swarat Chaudhuri, P. Madhusudan |
Languages of Nested Trees. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin |
Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Mikhail Bernadsky |
Bounded Model Checking for GSMP Models of Stochastic Real-Time Systems. |
HSCC |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Swarat Chaudhuri |
Branching Pushdown Tree Automata. |
FSTTCS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Insup Lee |
Preface. |
ACM Trans. Embedded Comput. Syst. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Kousha Etessami, Mihalis Yannakakis |
Realizability and verification of MSC graphs. |
Theor. Comput. Sci. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Michael Benedikt, Kousha Etessami, Patrice Godefroid, Thomas W. Reps, Mihalis Yannakakis |
Analysis of recursive state machines. |
ACM Trans. Program. Lang. Syst. |
2005 |
DBLP DOI BibTeX RDF |
recursive state machines, model checking, temporal logic, program analysis, Software verification, context-free languages, pushdown automata |
| 1 | Rajeev Alur, P. Madhusudan, Wonhong Nam |
Symbolic computational techniques for solving games. |
STTT |
2005 |
DBLP DOI BibTeX RDF |
QBF solving, Games, Formal verification, Symbolic model checking, Bounded model checking |
| 1 | Rajeev Alur, Kenneth L. McMillan, Doron Peled |
Deciding Global Partial-Order Properties. |
Formal Methods in System Design |
2005 |
DBLP DOI BibTeX RDF |
partial order logics, model checking, concurrency, temporal logics |
| 1 | Rajeev Alur |
The Benefits of Exposing Calls and Returns. |
CONCUR |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, P. Madhusudan |
On-the-Fly Reachability and Cycle Detection for Recursive State Machines. |
TACAS |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Viraj Kumar, P. Madhusudan, Mahesh Viswanathan |
Congruences for Visibly Pushdown Languages. |
ICALP |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Pavol Cerný, P. Madhusudan, Wonhong Nam |
Synthesis of interface specifications for Java classes. |
POPL |
2005 |
DBLP DOI BibTeX RDF |
behavioral interfaces, learning regular languages, model checking, games, abstraction, synthesis, software components |
| 1 | Rajeev Alur |
Trends and Challenges in Algorithmic Software Verification. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Hakan Yazarel, Antoine Girard, George J. Pappas, Rajeev Alur |
Quantifying the Gap between Embedded Control Models and Time-Triggered Implementations. |
RTSS |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, P. Madhusudan, Wonhong Nam |
Symbolic Compositional Verification by Learning Assumptions. |
CAV |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Salvatore La Torre, P. Madhusudan |
Perturbed Timed Automata. |
HSCC |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin |
Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement. |
VMCAI |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Arun Chandrashekharapuram |
Dispatch Sequences for Embedded Control Models. |
IEEE Real-Time and Embedded Technology and Applications Symposium |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Salvatore La Torre, George J. Pappas |
Optimal paths in weighted timed automata. |
Theor. Comput. Sci. |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Radu Grosu |
Modular refinement of hierarchic reactive machines. |
ACM Trans. Program. Lang. Syst. |
2004 |
DBLP DOI BibTeX RDF |
refinement, compositional semantics, assume-guarantee reasoning, Hierarchical state machines |
| 1 | Rajeev Alur, Salvatore La Torre |
Deterministic generators and games for Ltl fragments. |
ACM Trans. Comput. Log. |
2004 |
DBLP DOI BibTeX RDF |
Games, Temporal Logic, Automata |
| 1 | Rajeev Alur, David Arney, Elsa L. Gunter, Insup Lee, Jaime Lee, Wonhong Nam, Frederick Pearce, Stephen Van Albert, Jiaxiang Zhou |
Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System. |
STTT |
2004 |
DBLP DOI BibTeX RDF |
CARA system, Requirements formalization, Formal methods, Safety-critical systems, Software verification |
| 1 | Rajeev Alur, Sampath Kannan, Salvatore La Torre |
Polyhedral Flows in Hybrid Automata. |
Formal Methods in System Design |
2004 |
DBLP DOI BibTeX RDF |
polyhedral dynamics, hybrid systems, reachability analysis |
| 1 | Michael McDougall, Rajeev Alur, Carl A. Gunter |
A model-based approach to integrating security policies for embedded devices. |
EMSOFT |
2004 |
DBLP DOI BibTeX RDF |
policy integration, smartcards, model based design, Java cards |
| 1 | Rajeev Alur, Kousha Etessami, P. Madhusudan |
A Temporal Logic of Nested Calls and Returns. |
TACAS |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Zijiang Yang, Rajeev Alur |
Variable Reuse for Efficient Image Computation. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Mikhail Bernadsky, P. Madhusudan |
Optimal Reachability for Weighted Timed Games. |
ICALP |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Mikhail Bernadsky, Raman Sharykin, Rajeev Alur |
Structured Modeling of Concurrent Stochastic Hybrid Systems. |
FORMATS/FTRTFT |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur |
Games for Formal Design and Verification of Reactive Systems. |
ATVA |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, P. Madhusudan |
Decision Problems for Timed Automata: A Survey. |
SFM |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Doron Peled (eds.) |
Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings |
CAV |
2004 |
DBLP BibTeX RDF |
|
| 1 | Rajeev Alur, George J. Pappas (eds.) |
Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27, 2004, Proceedings |
HSCC |
2004 |
DBLP BibTeX RDF |
|
| 1 | Rajeev Alur, P. Madhusudan |
Visibly pushdown languages. |
STOC |
2004 |
DBLP DOI BibTeX RDF |
?-languages, verification, logic, context-free languages, pushdown automata, regular tree languages |
| 1 | Rajeev Alur, Kousha Etessami, Mihalis Yannakakis |
Inference of Message Sequence Charts. |
IEEE Trans. Software Eng. |
2003 |
DBLP DOI BibTeX RDF |
concurrent state machines, formal verification, synthesis, scenarios, requirements analysis, Message sequence charts, realizability, deadlock freedom |
| 1 | P. Madhusudan, Wonhong Nam, Rajeev Alur |
Symbolic computational techniques for solving games. |
Electr. Notes Theor. Comput. Sci. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Thao Dang, Joel M. Esposito, Yerang Hur, Franjo Ivancic, Vijay Kumar, Insup Lee, Pradyumna Mishra, George J. Pappas, Oleg Sokolsky |
Hierarchical modeling and analysis of embedded systems. |
Proceedings of the IEEE |
2003 |
DBLP BibTeX RDF |
|
| 1 | Rajeev Alur, Salvatore La Torre, P. Madhusudan |
Playing Games with Boxes and Diamonds. |
CONCUR |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, Sudipto Guha, Mihalis Yannakakis |
Compression of Partially Ordered Strings. |
CONCUR |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Insup Lee (eds.) |
Embedded Software, Third International Conference, EMSOFT 2003, Philadelphia, PA, USA, October 13-15, 2003, Proceedings |
EMSOFT |
2003 |
DBLP BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")