Publications of Rajeev Alur

Online Publications

Most of the papers available from this document appear in print, and the corresponding copyright is held by the publisher. While the papers can be used for personal use, redistribution or reprinting for commercial purposes is prohibited.

Recent Work

H. Zhang, K. Kallas, S. Pavlatos, R. Alur, S.Angel, and V. Liu. MuCache: A general framework for caching in microservice graphs, 21st USENIX Symp. on Networked Systems Design and Implementation (NSDI), 2024.
Z. Li, J. Huang, J. Liu, F. Zhu, E. Zhao, W. Dodds, N. Velingker, R. Alur, and M. Naik. Relational programming with foundation models, 38th AAAI Conf. on Artificial Intelligence (AAAI), 2024.
A. Xue, R. Alur, and E. Wong. Stability guarantees for feature attributions with multiplicative smoothing, 37th Conference on Neural Information Processing Systems (NeurIPS), 2023.
A. Thakkar, N. Sands, G. Petrou, R. Alur, M. Naik, and M. Raghothaman. Mobius: Synthesizing relational queries with recursive and invented predicates, OOPSLA, 2023.
R. Alur, O. Bastani, K. Jothimurugan, M. Perez, F. Somenzi, and A. Trivedi. Policy synthesis and reinforcement learning for discounted LTL, 35th International Conference on Computer-Aided Verification (CAV), 2023.
K. Jothimurugan, S. Hsu, O. Bastani, and R. Alur. Robust subtask learning for compositional generalization, 40th International Conference on Machine Learning (ICML), 2023.
R. Alur, C. Stanford, and C. Watson. A robust theory of series parallel graphs, 50th ACM Symposium on Principles of Programming Languages (POPL), 2023.
K. Kallas, H. Zhang, R. Alur, S. Angel, and V. Liu. Executing microservice applications on serverless, correctly, 50th ACM Symposium on Principles of Programming Languages (POPL), 2023.
A. Xue, L. Lindemann, A. Robey, H. Hassani, G.J. Pappas, and R. Alur. Chordal sparsity for Lipschitz constant estimation of deep neural networks, IEEE Conference on Decision and Control (CDC), 2022.
K. Jothimurugan, S. Bansal, O. Bastani, and R. Alur. Specification-guided learning of Nash equilibria with high social welfare, 34th International Conference on Computer-Aided Verification (CAV), 2022.
K. Kallas, F. Niksic, C. Stanford, and R. Alur. Stream processing with dependency-guided synchronization, 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), 2022.
L. Shi, Y. Wang, R. Alur, and B.T. Loo. Automatic repair for network programs, 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2022.
R. Alur, S. Bansal, O. Bastani, and K. Jothimurugan. A framework for transforming specifications in reinforcement learning, Principles of System Design: Essays dedicated to Thomas A. Henzinger on the occasion of his 60th birthday, 2022.
K. Jothimurugan, S.Bansal, O. Bastani, and R. Alur. Compositional reinforcement learning from logical specifications, 35th Conference on Neural Information Processing Systems (NeurIPS), 2021.
R. Ivanov, K. Jothimurugan, S. Hsu, S. Vaidya, R. Alur, and O. Bastani. Compositional learning and verification of neural network controllers, ACM SIGBED International Conference on Embedded Software (EMSOFT), 2021.
R. Ivanov, T. Carpenter, J. Weimer, R. Alur, G. Pappas, and I. Lee. Verisig 2.0: Verification of neural network controllers using Taylor model preconditiong, 33rd International Conference on Computer-Aided Verification (CAV), 2021.
A. Thakkar, A. Naik, N. Sands, R. Alur, M. Naik, and M. Raghothaman. Example-guided synthesis of relational queries, 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2021.
R. Alur, P. Hilliard, Z.G. Ives, K. Kallas, K. Mamouras, F. Niksic, C. Stanford, V. Tannen, and A. Xue. Synchronization schemas, ACM Symposium on Principles of Database Systems (PODS), Invited paper, 2021.
K. Jothimurugan, O. Bastani, and R. Alur. Abstract value iteration for hierarchical reinforcement learning, 24th International Conference on Artificial Intelligence and Statistics (AISTATS), 2021.
L. Shi, Y. Li, B.T. Loo, and R. Alur. Network traffic classification by program synthesis, 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2021.
K. Kallas, P. Niksic, C. Stanford, and R. Alur. DiffStream: Differential output testing for stream processing programs, OOPSLA, 2020. pdf
L. V. Nguyen, G. Mohan, J. Weimer, O. Sokolsky, I. Lee, and R. Alur. Reaffirm: Model-based repair of hybrid systems for improving resiliency, 18th ACM-IEEE International Conference on Formal Methods and Models for System Design, 2020. pdf
R. Alur, Y. Chen. K. Jothimurugan, and S. Khanna. Space-efficient query evaluation over probabilistic event streams, 35th ACM/IEEE Symposium on Logic in Computer Science, 2020. pdf
R. Ivanov, J. Weimer, R. Alur, G.J. Pappas, and I. Lee. Case Study: Verifying the Safety of an Autonomous Racing Car with a Neural Network Controller, 23rd ACM International Conference on Hybrid Systems: Computation and Control, 2020. pdf
R. Alur, D. Fisman, K. Mamouras, M. Raghothaman, and C. Stanford. Streamable regular transductions, Theoretical Computer Science, 2019. pdf
K. Jothimurugan, R. Alur, and O. Bastani. A Composable Specification Language for Reinforcement Learning Tasks, 33rd Conference on Neural Information Processing Systems, 2019. pdf
L. V. Nguyen, G. Mohan, J. Weimer, O. Sokolsky, I. Lee, and R. Alur. Detecting Security Leaks in Hybrid Systems with Information Flow Analysis, 17th ACM-IEEE International Conference on Formal Methods and Models for System Design, 2019. pdf
K. Mamouras, C. Stanford, R. Alur, Z. Ives, and V. Tannen. Data-trace types for distributed stream processing systems, ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019. pdf
R. Ivanov, J. Weimer, R. Alur, G.J. Pappas, and I. Lee. Verisig: Verifying safety properties of hybrid systems with neural network controllers, 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019. pdf
R. Alur, K. Mamouras, and C. Stanford. Modular quantitative monitoring, 46th ACM Symposium on Principles of Programming Languages, 2019. pdf
H. Abbas, R. Alur, K. Mamouras, R. Mangharam, and A. Rodionova. Real-time decision policies with predictable performance, Proceedings of the IEEE, 2018. pdf
R. Alur, D. Fisman, R. Singh, A. Solar-Lezama. Search-based program synthesis, Communications of the ACM, 2018. pdf
R. Alur, J. Deviette, and N. Singhania. Block-size independence for GPU programs, 25th Static Analysis Symposium, 2018. pdf
W. Lee, K. Heo, R. Alur, and M. Naik. Accelerating search-based program synthesis using learned probabilistic models, ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018. pdf
Y. Yuan, D. Lin, A. Mishra, S. Marwaha, R. Alur, and B.-T. Loo. Quantitative network monitoring with NetQRE, ACM SIGCOMM, 2017. pdf
R. Alur and L. D'Antoni. Streaming tree transducers, Journal of the ACM, 2017. pdf
R. Alur, J. Deviette, O. Navarro Leija, and N. Singhania. GPUDrano: Detecting uncoalesced accesses in GPU programs, 28th International Conference on Computer-Aided Verification, 2017. pdf
R. Alur, K. Mamouras, and C. Stanford. Automata-based stream processing, 44th Intl. Colloq. on Automata, Languages, and Programming, 2017. pdf
R. Alur, K. Mamouras, and D. Ulus. Derivatives of quantitative regular expressions, Models, Algorithms, Logics and Tools: Essays dedicated to Kim G. Larsen 2017. pdf
K. Mamouras, M. Raghothaman, R. Alur, Z. Ives, and S. Khanna. StreamQRE: Modular specification and efficient evaluation of quantitative queries over streaming data, ACM Conference on Programming Language Design and Implementation, 2017. pdf
R. Alur, A. Radhakrishna, and A. Udupa. Scaling enumerative program synthesis via divide and conquer, 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2017. pdf
R. Alur and S. Tripakis. Atomatic synthesis of distributed protocols, SIGACT News, 2017. pdf
R. Alur, M. Faella, S. Kannan, and N. Singhania. Hedging bets in Markov decision processes, 25th EACSL Annual Conference on Computer Science Logic, 2016. pdf
R. Alur et al. Computer-Aided Personalized Education: CCC Visioning Workshop Report, 2016. pdf
R. Alur, S. Moarref, and U. Topcu. Compositional synthesis of reactive controllers for multi-agent systems, 27th International Conference on Computer-Aided Verification, 2016. pdf
R. Alur, D. Fisman, and M. Raghothaman. Regular programming for quantitative properties of data streams, 25th European Symposium on Programming, 2016. pdf
R. Alur, S. Moarref, and U. Topcu. Compositional synthesis with parametric reactive controllers, 19th ACM International Conference on Hybrid Systems: Computation and Control, 2016. pdf
R. Alur and D. Fisman. Colored nested words, 10th International Conference on Language and Automata Theory and Applications, 2016. pdf
Y. Yuan, D. Lin, R. Alur, and B.T. Loo. Scenario-based programming for SDN policies, 11th Conference on Emerging Networking Experiments and Technologies (CoNeXT), 2015. pdf
L. D'Antoni, M. Weaver, A. Weinert, and R. Alur. Automata Tutor and what we learned from building an online teaching tool, The Bulletin of the EATCS 117, 2015. pdf
R. Alur, P. Cerny, and A. Radhakrishna. Synthesis through unification, 27th International Conference on Computer-Aided Verification, 2015. pdf
R. Alur, M. Raghothaman, C. Stergiou, S. Tripakis, and A. Udupa. Automatic completion of distributed protocols with symmetry, 27th International Conference on Computer-Aided Verification, 2015. pdf
L. D'Antoni, D. Kini, R. Alur, S. Gulwani, M. Viswanathan, and B. Hartmann. How can automatic feedback help students construct automata?, ACM Transactions on Comuter-Human Interaction, Vol. 22, No. 2, Article 9, 2015. pdf
R. Alur, S. Moarref, and U. Topcu. Pattern-based refinement of assume-guarantee specifications in reactive synthesis, 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2015. pdf
R. Alur, L. D'Antoni, and M. Raghothaman. DReX: A declarative language for efficiently evaluating regular string transformations, 42nd ACM Symposium on Principles of Programming Languages, 2015. pdf
R. Alur, T.A. Henzinger, and M.Y. Vardi. Theory in Practice for System Design and Verification, SIGLOG News 2015. pdf
Y. Yuan, R. Alur, and B.-T. Loo. NetEgg: Programming network policies by examples, 13th ACM Workshop on Hot Topics in Networks, 2014. pdf
R. Alur, M.M.K. Martin, M. Raghothaman, C. Stergiou, S. Tripakis, and A. Udupa. Synthesizing finite state protocols from scenarios and requirements, 10th Haifa Verification Conference, 2014. pdf
R. Alur and N. Singhania. Precise piecewise affine models from input-output data., 14th ACM Intl. Conf. on Embedded Software, 2014. pdf
R. Alur, A. Freilich, and M. Raghothaman. Regular combinators for string transformations, 29th ACM/IEEE Symposium on Logic in Computer Science, 2014. pdf
L. D'Antoni and R. Alur. Symbolic Visibly Pushdown Automata, 26th International Conference on Computer-Aided Verification, 2014. pdf
R. Alur, A. Bouajjani, and J. Esparza. Model checking procedural programs, Handbook of Model Checking, Springer, 2014. pdf
R. Alur, R. Bodik, G. Juniwal, M.M.K. Martin, M. Raghothaman, S.A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa. Syntax-guided Synthesis, 13th International Conference on Formal Methods in Computer-Aided Design, 2013. pdf
R. Alur, S. Moarref, and U. Topcu. Counter-strategy guided refinement of GR(1) temporal logic specifications, 13th International Conference on Formal Methods in Computer-Aided Design, 2013. pdf
Y. Yuan, A. Wang, R. Alur, and B.T. Loo. On the feasibility of automation for bandwidth allocation problems in data centers, 13th International Conference on Formal Methods in Computer-Aided Design, 2013. pdf
R. Alur, L. D'Antoni, J. Deshmukh, M. Raghothaman, and Y. Yuan. Regular functions and cost register automata, 28th ACM/IEEE Symposium on Logic in Computer Science, 2013. pdf
R. Alur, A. Durand-Gasselin, and A. Trivedi. From Monadic Second-Order definable string transformations to transducers, 28th ACM/IEEE Symposium on Logic in Computer Science, 2013. pdf
R. Alur and M. Raghothaman. Decision problems for additive regular functions, 40th International Colloquium on Automata, Languages, and Programming, 2013. pdf
R. Alur, L. D'Antoni, S. Gulwani, D. Kini, and M. Viswanathan. Automated grading of DFA constructions, International Joint Conference on Artifical Intelligence, 2013. pdf
A. Udupa, A. Raghavan, J. Deshmukh, S. Mador-Haim, M.M.K. Martin, and R. Alur. TRANSIT: Specifying protocols with concolic snippets, ACM Conference on Programming Language Design and Implementation, 2013. pdf
J. Thakkar, A. Kanade, and R. Alur. Transducer-based algorithmic verification of retransmission protocols over noisy channels, IFIP Joint International Conference on Formal Techniques for Distributed Systems, 2013. pdf
R. Alur,V. Forejt, S. Moarref, and A. Trivedi. Safe schedulability of bounded-rate multi-mode systems, 16th International Conference on Hybrid Systems: Computation and Control, 2013. pdf
R. Alur, S. Kannan, K. Tian, and Y. Yuan. On the complexity of shortest path problems on discounted cost graphs, 7th International Conference on Language and Automata Theory and Applications, 2013. pdf
S. Mador-Haim, L. Maranget, S. Sarkar, K. Memarian, J. Alglave, S. Owens, R. Alur, M. Martin, P. Sewell, and D. Williams. An axiomatic memory model for POWER multiprocessors, 24th International Conference on Computer-Aided Verification, 2012. pdf
R. Alur, E. Filiot, and A. Trivedi. Regular transformations of infinite strings, 27th ACM/IEEE Symposium on Logic in Computer Science, 2012. pdf
R. Alur, A. Trivedi, and D. Wojtczak. Optimal scheduling for constant-rate multi-mode systems, 15th International Conference on Hybrid Systems: Computation and Control, 2012. pdf
Z. Jiang, M. Pajic, S. Moarref, R. Alur, and R. Mangharam. Modeling and verification of a dual chamber implantable pacemaker, 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2012. pdf
R. Alur. Formal verification of hybrid systems, 11th International Conference on Embedded Software, 2011. pdf
R. Alur and A. Trivedi. Relating average and discounted costs for quantitative analysis of timed systems, 11th International Conference on Embedded Software, 2011. pdf
R. Alur and J. Deshmukh. Nondeterministic streaming string transducers, 38th International Colloquium on Automata, Languages, and Programming, 2011. Updated version: pdf
S. Mador-Haim, R. Alur, and M.M.K. Martin. Litmus tests for comparing memory consistency models: How long do they need to be?, 47th Design Automation Conference, 2011. pdf
R. Alur and P. Cerny. Expressiveness of streaming string transducers, Invited paper at 30th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2010. pdf
R. Alur and P. Cerny. Streaming transducers for algorithmic verification of single-pass list processing programs, 38th ACM Symposium on Principles of Programming Languages, 2011. pdf
A. Kanade, R. Alur, S. Rajamani, and G. Ramalingam. Representation dependence testing using program inversion, 18th ACM SIGSOFT International Symposium on the Foundations of Software Engineering, 2010. pdf
S. Mador-Haim, R. Alur, and M.M.K. Martin. Generating litmus tests for contrasting memory consistency models, 22nd International Conference on Computer-Aided Verification, 2010. pdf
P. Cerny, A. Radhakrishnan, D. Zufferey, S. Chaudhuri, and R. Alur. Model checking of linearizability of concurrent list implementations, 22nd International Conference on Computer-Aided Verification, 2010. pdf
R. Alur and S. Chaudhuri. Temporal reasoning for procedural programs, 11th International Conference on Verification, Model Checking, and Abstract Interpretation, 2010. pdf
G. Weiss, A. D'Innocenzo, R. Alur, K.H. Johansson, and G.J. Pappas. Robust stability of multi-hop networks, 48th IEEE Conference on Decision and Control, 2009. pdf
R. Alur, P. Cerny, and S. Weinstein. Algorithmic analysis of array-accessing programs, 18th EACSL Annual Conference on Computer Science Logic, 2009. pdf
P. Cerny and R. Alur. Automated analysis of Java methods for confidentiality, 21st International Conference on Computer-Aided Verification, 2009. pdf
A. Kanade, R. Alur, F. Ivancic, S. Ramesh, S. Sankaranarayanan, and K.C. Shashidhar. Generating and analyzing symbolic traces of Simulink/Stateflow models, 21st International Conference on Computer-Aided Verification, 2009. pdf
R. Alur and P. Madhusudan. Adding nesting structure to words, Journal of the ACM, 2009. pdf
R. Alur, A. Degorre, O. Maler, and G. Weiss. On Omega-languages defined by mean-payoff conditions, 12th International Conference on Foundations of Software Science and Computation Structures, 2009. pdf
G. Weiss, S. Fischmeister, M. Anand, and R. Alur. Specification and analysis of network resource requirements of control systems, 12th International Conference on Hybrid Systems: Computation and Control, 2009. pdf
R. Alur, A. D'Innocenzo, K. Johansson, G. Pappas, and G. Weiss Modeling and analysis of multi-hop control networks, 15th IEEE Real-Time and Embedded Technology and Applications Symposium, 2009. pdf
R. Alur and G. Weiss. RTComposer:A framework for real-time components with scheduling interfaces, 8th ACM/IEEE Conference on Embedded Software, 2008. pdf
R. Alur, A. Kanade, S. Ramesh, and K. Shashidhar. Symbolic analysis for improving simulation coverage of Simulink/Stateflow models, 8th ACM/IEEE Conference on Embedded Software, 2008. pdf
R. Alur, A. Kanade, and G. Weiss. Ranking automata and games for prioritized requirements, 20th International Conference on Computer-Aided Verification, 2008. pdf
R. Alur and G. Weiss. Regular specifications of resource requirements for embedded control software, 14th IEEE Real-Time and Embedded Technology and Applications Symposium, 2008. pdf
S. Chaudhuri and R. Alur. Instrumenting C programs with nested word monitors, 14th International workshop on Model Checking Software (SPIN), 2007. pdf
R. Alur, M. Arenas, P. Barcelo, K. Etessami, N. Immerman, and L. Libkin. First-order and temporal logics for nested words, 22nd IEEE Symposium on Logic in Computer Science, 2007. Journal version
S. Burckhardt, R. Alur, and M.M.K. Martin. Checkfence: Checking consistency of concurrent data types on relaxed memory models, ACM Conference on Programming Language Design and Implementation, 2007. pdf
R. Alur. Marrying words and trees, 26th ACM Symposium on Principles of Database Systems, 2007. pdf
R. Alur, P. Cerny, and S. Chaudhuri. Model checking on trees with path equivalences, 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2007. pdf
G. Weiss and R. Alur. Automata based interfaces for control and scheduling, 10th International Conference on Hybrid Systems: Computation and Control, 2007. pdf
M. Bernadsky and R. Alur. Symbolic analysis of GSMP models with one stateful clock, 10th International Conference on Hybrid Systems: Computation and Control, 2007. pdf
R. Alur and S. Chaudhuri. Branching pushdown tree automata, 26th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2006. pdf
T. Nghiem, G. Pappas, A. Girard, and R. Alur. Time-triggered implementations of dynamic controllers, 6th Annual ACM Conference on Embedded Software, 2006. pdf
W. Nam and R. Alur. Learning-based symbolic assume-guarantee reasoning with automatic decomposition, Fourth International Symposium on Automated Technology for Verification and Analysis, 2006.pdf
S. Burckhardt, R. Alur, and M. Martin. Bounded model checking of concurrent data types on relaxed memory models: A case study, 18th International Conference on Computer-Aided Verification, 2006. pdf
R. Alur, S. Chaudhuri, and P. Madhusudan. Languages of nested trees, 18th International Conference on Computer-Aided Verification, 2006. pdf
R. Alur, P. Cerny, and S. Zdancewic. Preserving secrecy under refinement, 33rd International Colloquium on Automata, Languages, and Programming, 2006.pdf
R. Alur and M. Bernadsky. Bounded model checking of GSMP models of stochastic real-time systems, Ninth International Conference on Hybrid Systems: Computation and Control, 2006. pdf
R. Alur, S. Chaudhuri, and P. Madhusudan. A fixpoint calculus for local and global program flows, 33rd ACM Symposium on Principles of Programming Languages, 2006. pdf
H. Yazarel, A. Girard, G. Pappas and R. Alur. Quantifying the gap between embedded control models and time-triggered implementations, 26th IEEE Real-Time Systems Symposium, 2005 pdf
R. Alur, P. Madhusudan, and W. Nam. Symbolic compositional verification by learning assumptions, 17th International Conference on Computer-Aided Verification, 2005. pdf
R. Alur, V. Kumar, P. Madhusudan, and M. Viswanathan. Congruences for visibly pushdown languages, 32nd International Colloquium on Automata, Languages, and Programming, 2005.pdf
R. Alur, S. Chaudhuri, K. Etessami, and P. Madhusudan. On-the-fly reachability and cycle detection for recursive state machines, 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2005. ps
R. Alur, S. La Torre and P. Madhusudan. Perturbed timed automata, Eighth International Conference on Hybrid Systems: Computation and Control, 2005. ps
R. Alur and A. Chandrashekharapuram. Dispatch sequences for embedded control models, 11th IEEE Real-Time and Embedded Technology and Applications Symposium, 2005. Extended version to appear in Special issue of JCSS
S. Burckhardt, R. Alur, and M. Martin. Verifying safety of a token coherence implementation by parametric compositional refinement, Sixth International Conference on Verification, Model Checking, and Abstract Interpretation, 2005. pdf
R. Alur, P. Cerny, P. Madhusudan, and W. Nam. Synthesis of interface specifications for Java classes, 32nd ACM Symposium on Principles of Programming Languages, 2005. pdf
Z. Yang and R. Alur. Variable reuse for efficient image computation, 5th International Conference on Formal Methods in Computer-Aided Design, 2004. pdf
M. McDougall, R. Alur, and C.A. Gunter. A model-based approach to integrating security policies for embedded devices, Fifth ACM Conference on Embedded Software, 2004. pdf
M. Bernadsky, R Sharykin, and R. Alur. Structured modeling of concurrent stochastic hybrid systems, Joint Conference on Formal Modeling and Analysis of Timed Systems and Formal Techniques in Real-Time and Fault Tolerant Systems, 2004. ps
R. Alur, M. Bernadsky, and P. Madhusudan. Optimal reachability for weighted timed games, 31st International Colloquium on Automata, Languages, and Programming, 2004.Extended and revised version
R. Alur and P. Madhusudan. Visibly pushdown languages, 36th ACM Symposium on Theory of Computing, 2004. Extended and revised version (pdf)
R. Alur, K. Etessami, and P. Madhusudan. A temporal logic of nested calls and returns, Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2004. pdf
R. Alur, S. La Torre, and P. Madhusudan. Playing games with boxes and diamonds, 14th International Conference on Concurrency Theory, 2003 pdf
R. Alur, S. Chaudhuri, K. Etessami, S. Guha, and M. Yannakakis. Compression of partially ordered strings, 15th International Conference on Concurrency Theory, 2003 ps
P. Madhusudan, W. Nam, and R. Alur. Symbolic computational techniques for solving games, To appear in Software Tools for Technology Transfer, ps
R. Alur, S. La Torre, and P. Madhusudan. Modular strategies for infinite games on recursive game graphs, 15th International Conference on Computer-Aided Verification, 2003. ps
R. Alur, F. Ivancic, J. Kim, I. Lee, and O. Sokolsky. Generating embedded software from hierarchical hybrid models, ACM Symposium on Languages, Compilers, and Tools for Embedded Systems, 2003. pdf
R. Alur, S. La Torre, and P. Madhusudan. Modular strategies for recursive game graphs, Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2003. pdf
R. Alur, T. Dang, and F. Ivancic. Counter-example guided predicate abstraction of hybrid systems, Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2003. pdf, Extended and revised version to appear in ACM Transactions on Embedded Compuetr Systems
R. Alur, T. Dang, and F. Ivancic. Progress on reachability analysis of hybrid systems using predicate abstraction, Sixth International Conference on Hybrid Systems: Computation and Control, 2003. pdf
R. Alur, C. Belta, F. Ivancic, V. Kumar, H. Rubin, J. Schug, O. Sokolsky, and J. Webb. Visual programming for modeling and simulation of biomolecular regulatory networks, International Conference on High Performance Computing, 2002. pdf
A. Goodloe, M. McDougall, C. Gunter and R. Alur. Predictable programs in barcodes, International Conference on Compilers, Architecture and Synthesis of Embedded Systems (CASES), 2002. pdf
R. Alur, M. McDougall and Z. Yang. Exploiting behavioral hierarchy for efficient model checking, 14th International Conference on Computer-Aided Verification, 2002. pdf
R. Alur, T. Dang, and F. Ivancic. Reachability analysis of hybrid systems via predicate abstraction, Fifth International Workshop on Hybrid Systems: Computation and Control, 2002. pdf
R. Alur and R. Grosu. Shared variables interaction diagrams, 16th IEEE International Conference on Automated Software Engineering, 2001. pdf
R. Alur, T. Dang, J. Esposito, Y. Hur, F. Ivancic, V. Kumar, I. Lee, P. Mishra, G. Pappas, O. Sokolsky. Hierarchical Modeling and Analysis of Embedded Systems, First Workshop on Embedded Software, 2001. Extended version to appear in a special issue of Proceedings of the IEEE.
O. Moller and R. Alur. Heuristics for hierarchical partitioning with applications to model checking, 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, 2001. Abstract. ps
R. Alur, K. Etessami, and M. Yannakakis. Analysis of recursive state machines, 13th International Conference on Computer-Aided Verification, 2001. Abstract. ps Extended version in ACM TOPLAS with Benedikt, Etessami, Godefroid, Reps, Yannakakis
R. Alur and B.-Y. Wang. Verifying network protocol implementations by symbolic refinement checking, 13th International Conference on Computer-Aided Verification, 2001. Abstract. ps
R. Alur and S. La Torre. Deterministic generators and games for LTL fragments, 16th IEEE Symposium on Logic in Computer Science, 2001. Abstract. Revised and extended version, to appear in ACM Transactions on Computational Logic.
R. Alur, K. Etessami, and M. Yannakakis. Realizability and verification of MSC graphs, 28th International Colloquium on Automata, Languages, and Programming, 2001. Abstract. Extended and revised version to appear in Theoretical Computer Science.
R. Alur, L. de Alfaro, R. Grosu, T.A. Henzinger, M. Kang, R. Majumdar, F. Mang, C.M. Kirsch, and B.-Y. Wang. Mocha: A model checking tool that exploits design structure, 23rd International Conference on Software Engineering, pp. 835--836, 2001. ps
R. Alur, C. Belta, F. Ivancic, V. Kumar, M. Mintz, G. Pappas, H. Rubin, and J. Schug. Hybrid modeling and simulation of biomolecular networks, Fourth International Workshop on Hybrid Systems: Computation and Control, LNCS 2034, pp. 19--32, 2001. ps
R. Alur, S. La Torre, and G. Pappas. Optimal paths in weighted timed automata, Fourth International Workshop on Hybrid Systems: Computation and Control, LNCS 2034, pp. 49--62, 2001. Abstract. ps
R. Alur, R. Grosu, I. Lee, and O. Sokolsky. Compositional refinement of hierarchical hybrid systems, Fourth International Workshop on Hybrid Systems: Computation and Control, LNCS 2034, pp. 33--48, 2001. Abstract. ps
R. Alur, A. Das, J. Esposito, R. Fierro, Y. Hur, G. Grudic, V. Kumar, I. Lee, J. P. Ostrowski, G. Pappas, J. Southall, J. Spletzer, and C. Taylor. A framework and architecture for multirobot coordination, Seventh International Symposium on Experimental Robotics, 2001. pdf
R. Alur, R. Grosu, and B.-Y. Wang. Automated refinement checking for asynchronous processes. 3rd International Conference on Formal Methods in Computer-Aided Design, 2000. Abstract. ps
R. Alur, R. Grosu, and M. McDougall. Efficient reachability analysis of hierarchic reactive machines, 12th International Conference on Computer-Aided Verification, LNCS 1855, pp. 280--295, 2000. Abstract. ps
R. Alur, K. Etessami, and M. Yannakakis. Inference of message sequence charts, 22nd International Conference on Software Engineering, pp. 304--313, 2000. Abstract. Revised and extended version: pdf
R. Alur, R. Grosu, Y. Hur, V. Kumar, and I. Lee. Modular specifications of hybrid systems in CHARON, Proceedings of Third Intl. Workshop on Hybrid Systems: Computation and Control, LNCS 1790, pp. 6--19, 2000. Abstract. ps
R. Alur and R. Grosu. Modular refinement of hierarchic state machines, Proceedings of the 27th ACM Symposium on Principles of Programming Languages, pp. 390--402, 2000. Abstract. ps
R. Alur, J. Esposito, M. Kim, V. Kumar, and I. Lee. Formal modeling and analysis of hybrid systems: A case study in multirobot coordination, FM'99: Proceedings of the World Congress on Formal Methods, LNCS 1708, pp. 212--232, Springer, 1999. Abstract. ps
R. Alur, L. de Alfaro, T. Henzinger, and F. Mang. Automating modular verification, Proceedings of the Tenth International Conference on Concurrency Theory, LNCS 1664, Springer, pp. 82--97, 1999. Abstract. ps
R. Alur and B.-Y. Wang. ``Next'' heuristic for on-the-fly model checking, Proceedings of the Tenth International Conference on Concurrency Theory, LNCS 1664, Springer, pp. 98--113, 1999. Abstract. ps
R. Alur and M. Yannakakis. Model checking of message sequence charts, Proceedings of the Tenth International Conference on Concurrency Theory, LNCS 1664, Springer, pp. 114--129, 1999. Abstract. ps
R. Alur, S. Kannan, and M. Yannakakis. Communicating hierarchical state machines, Proceedings of the 26th International Colloquium on Automata, Languages, and Programming, LNCS 1644, Springer, pp. 169--178, 1999. Abstract. Extended and revised version
R. Alur, K. Etessami, S. La Torre, and D. Peled. Parametric temporal logic for model measuring, Proceedings of the 26th International Colloquium on Automata, Languages, and Programming, LNCS 1644, Springer, pp. 159--168, 1999. Abstract. Extended version (to appear in ACM Trans. on Computational Logic)
R. Alur, S. Kannan, and S. La Torre. Polyhedral flows in hybrid automata, Proceedings of the Second International Conference on Hybrid Systems: Computation and Control, LNCS 1599, pp. 5-18, 1999. Springer. Abstract. Full version to appear in Formal Methods in System Design
R. Alur and D. Peled. Undecidability of partial order logics, Information Processing Letters 69(3), 1999. Abstract. ps
R. Alur, R. Kurshan, and M. Viswanathan. Membership problems for timed and hybrid automata, 19th IEEE Real-Time Systems Symposium, 1998. Abstract. ps
R. Alur and M. Yannakakis. Model checking of hierarchical state machines. Sixth ACM Symposium on the Foundations of Software Engineering, pp. 175-188, 1998. Abstract. Revised and extended version appears in ACM TOPLAS, 2001).
R. Alur, T.A. Henzinger, F.Y.C. Mang, S. Qadeer, S.K. Rajamani, S. Tasiran. MOCHA: modularity in model checking. Tenth International Conference on Computer-Aided Verification, LNCS 1427, pp. 516-520, 1998. Springer-Verlag. ps.
R. Alur, T.A. Henzinger, O. Kupferman, M.Y. Vardi. Alternating refinement relations. Ninth International Conference on Concurrency Theory, LNCS 1466, pp. 163-178, 1998. Springer-Verlag. Abstract. ps
R. Alur, K. McMillan, D. Peled. Deciding global partial-order properties. 25th International Colloquium on Automata, Languages, and Programming, LNCS 1443, pp. 41-52, 1998. Springer-Verlag. Abstract. ps
R. Alur, T.A. Henzinger, O. Kupferman. Alternating-time temporal logic. 38th IEEE Symposium on Foundations of Computer Science, pp. 100-109, 1997. Abstract. Proceedings version. An extended version appears in Compositionality -- The Significant Difference, LNCS 1536, pp. 23-60, Springer-Verlag, 1999. Revised and extended version, to appear in Journal of the ACM, 2002
R. Alur, T.A. Henzinger, S.K. Rajamani. Symbolic exploration of transition hierarchies. Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1384, pp. 330-344, 1998. Springer Verlag. Abstract. ps
R. Alur. Model checking: From tools to theory, 25MC: 25 Years of Model Checking, 2007. pdf
R. Alur and S. Chaudhuri. Logics and automata for software model checking, Marktoberdorf Summer School, 2006. pdf
R. Alur and P. Madhusudan. Decision problems for timed automata: A survey, 4th Intl. School on Formal Mthods for Computer, Communication, and Software Systems: Real Time, 2004 ps
R. Alur. Formal analysis of hierarchical state machines, International Symposium on Verification in Honor of Zohar Manna, 2003 pdf
R. Alur, T. Henzinger, G. Lafferriere, and G. Pappas. Discrete abstractions of hybrid systems. Proceedings of the IEEE, 2000.
R. Alur. Timed Automata. NATO-ASI 1998 Summer School on Verification of Digital and Hybrid Systems. A revised and shorter version appears in 11th International Conference on Computer-Aided Verification, LNCS 1633, pp. 8-22, Springer-Verlag, 1999.
R. Alur, T.A. Henzinger, H. Wong-Toi. Symbolic analysis of hybrid systems. Proceedings of the 37th IEEE Conference on Decision and Control, Invited survey, 1997.
R. Alur and T.A. Henzinger. Logics and Models of Real Time: A Survey. In Real-Time: Theory in Practice, REX Workshop, LNCS 600, pp. 74-106, 1991. Abstract. Full paper.
R. Alur and T.A. Henzinger. Modularity for timed and hybrid systems. Proceedings of the Ninth International Conference on Concurrency Theory, LNCS 1243, pp. 74--88, 1997. Abstract. Full paper.
R. Alur and T.A. Henzinger. Reactive modules. Proceedings of the 11th IEEE Symposium on Logic in Computer Science, pp. 207-218, 1996. Abstract. Full paper.
R. Alur and T.A. Henzinger. Local liveness for compositional modeling of fair reactive systems. Proceedings of the Seventh International Conference on Computer-aided Verification, LNCS 939, pp. 166-179, 1995. Abstract. Full paper.
R. Alur and T.A. Henzinger. Real-Time System = Discrete System + Clock Variables. In Theories and Experiences for Real-Time System Development, AMAST Series in Computing, pp. 1-30, 1994. Abstract. Full paper.
R. Alur and T.A. Henzinger. Finitary fairness. Proceedings of the Ninth IEEE Symposium on Logic in Computer Science, pp. 52-61, 1994. Abstract. Full paper.
R. Alur and D.L. Dill. Automata-theoretic verification of real-time systems. In Formal Methods for Real-Time Computing, Trends in Software Series, John Wiley & Sons Publishers, pp. 55-82, 1996. Abstract. Full paper.
R. Alur, L. Fix, T.A. Henzinger. Event-clock automata: A determinizable class of timed automata. Proceedings of the Sixth Conference on Computer-Aided Verification, LNCS 818, pp. 11-13, 1994 (to appear in Theoretical Computer Science). Abstract. Full paper.
R. Alur, C. Courcoubetis, T.A. Henzinger. The observational power of clocks. Proceedings of the Fifth Conference on Concurrency Theory, LNCS 836, pp. 162-177, 1994. Abstract. Full paper.
R. Alur, C. Courcoubetis, T.A. Henzinger. Computing accumulated delays in real-time systems. Proceedings of the Fifth Conference on Computer-Aided Verification, LNCS 697, pp. 181-193, 1993 (to appear in Formal Methods in System Design). Abstract. Full paper.
R. Alur, T.A. Henzinger, M.Y. Vardi. Parametric real-time reasoning. Proceedings of the 25th ACM Symposium on Theory of Computing, pp. 592-601, 1993. Abstract. Full paper.
R. Alur, C. Courcoubetis, D.L. Dill, N. Halbwachs, H. Wong-Toi. Minimization of timed transition systems. Proceedings of the Third Conference on Concurrency Theory, LNCS 630, pp. 340-354, 1992. Full paper.
R. Alur and T.A. Henzinger. Back to the future: Towards a theory of timed regular languages. Proceedings of the 33rd IEEE Symposium on Foundations of Computer Science, pp. 177-186, 1992. Abstract. Full paper.
R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science 126:183-235, 1994 (preliminary versions appeared in Proc. 17th ICALP, LNCS 443, 1990, and Real Time: Theory in Practice, LNCS 600, 1991). Abstract. Full paper.
R. Alur, L.J. Jagadeesan, J.J. Kott, and J.E. Von Olnhausen. Model-checking of real-time systems: a telecommunications application. Proceedings of the International Conference on Software Engineering, 1997. Abstract. Full paper.
S. Tasiran, R. Alur, R.P. Kurshan, and R.K. Brayton. Verifying abstractions of timed systems. Proceedings of the Seventh Conference on Concurrency Theory, LNCS 1119, 1996. Abstract. Full paper.
R. Alur and R.P. Kurshan. Timing analysis in COSPAN. Hybrid Systems III: Verification and Control, LNCS 1066, pp. 220-231, 1996. Abstract. Full paper.
R. Alur, C. Courcoubetis, D.L. Dill, N. Halbwachs, H. Wong-Toi. An implementation of three algorithms for timing verification based on automata emptiness. Proceedings of the 13th IEEE Real-Time Systems Symposium, pp. 157-166, 1992. Full paper.
R. Alur, A. Itai, R.P. Kurshan, M. Yannakakis. Timing verification by successive approximation. Information and Computation 118(1):142-157, 1995 (preliminary version appeared in Proc. 4th CAV, LNCS 663, 1992). Abstract. Full paper.
R. Alur, T.A. Henzinger, P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Trans. on Software Engineering 22(3):181-201, 1996 (preliminary version appeared in Proc. 14th RTSS, 1993). Abstract. Full paper.
R. Alur, C. Coucoubetis, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science 138:3-34, 1995 (preliminary version appeared in Proc. Conf. on Analysis and Optimization of Systems: Discrete-event Systems, LNCIS 199, 1994). Abstract. Full paper.
R. Alur, C. Courcoubetis, T.A. Henzinger, P.-H. Ho. Hybrid Automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid Systems, LNCS 736, pp. 209-229, 1993. Abstract. Full paper.
R. Alur, C. Courcoubetis, M. Yannakakis. Distinguishing tests for nondeterministic and probabilistic machines. Proceedings of the 27th ACM Symposium on Theory of Computing, pp. 363-372, 1995. Abstract. Full paper.
R. Alur, C. Courcoubetis, D.L. Dill. Verifying automata specifications of probabilistic real-time systems. In Real-Time: Theory in Practice, REX Workshop, LNCS 600, pp. 28-44, 1991. Abstract. Full paper.
R. Alur, C. Courcoubetis, D.L. Dill. Model-checking for probabilistic real-time systems. Automata, Languages and Programming: Proceedings of the 18th ICALP, LNCS 510, pp. 115-136, 1991. Abstract. Full paper.
R. Alur, G.J. Holzmann, D. Peled. An analyzer for message sequence charts. Software Concepts and Tools, 17(2):70-77, 1996 (preliminary version appeared in Proc. 2nd TACAS, LNCS 1055, 1996). Abstract. Full paper.
R. Alur, R.K. Brayton, T.A. Henzinger, S. Qadeer, and S.K. Rajamani. Partial-order reduction in symbolic state-space exploration. Proceedings of the Ninth International Conference on Computer-aided Verification, LNCS 1254, pp. 340--351, 1997. Abstract. Full paper.
R. Alur, K.L. McMillan, D.A. Peled. Model-checking of correctness conditions for concurrent objects. Proceedingss of the 11th IEEE Symposium on Logic in Computer Science, pp. 219-228, 1996. Abstract. Full paper.
R. Alur, D.A. Peled, W. Penczek. Model-checking of causality properties. Proceedingss of the Tenth IEEE Symposium on Logic in Computer Science, pp. 90-100, 1995. Abstract. Full paper.
R. Alur and G. Taubenfeld. Fast timing-based algorithms. Distributed Computing 10(1):1-10, 1996 (preliminary version appeared in Proc. 13th RTSS, 1992). Abstract. Full paper.
R. Alur and G. Taubenfeld. Contention-free complexity of shared memory algorithms. Information and Computation 126(1):62-73, 1996 (preliminary version appeared in Proc. 13th PODC, 1994). Abstract. Full paper.
R. Alur and T.A. Henzinger. A really temporal logic. Journal of the ACM 41:181-204, 1994 (preliminary version appeared in the Proc. 30th FOCS 1989). Abstract. Full paper.
R. Alur, H. Attiya, G. Taubenfeld. Time-adaptive algorithms for synchronization. SIAM J. on Computing 26(2):539-556, 1997 (preliminary version appeared in Proc. 25th STOC, 1994). Abstract. Full paper.
R. Alur and G. Taubenfeld. How to share a data structure: A fast timing-based solution. Proceedings of the Fifth IEEE Symposium on Parallel and Distributed Processing, pp. 470-477, 1993. Abstract. Full paper.
R. Alur, T. Feder, T.A. Henzinger. The benefits of relaxing punctuality. Journal of the ACM 43:116-146, 1996 (preliminary version appeared in Proc. 10th PODC, 1991). Abstract. Full paper.
R. Alur, C. Courcoubetis, D.L. Dill. Model-checking in dense real-time. Information and Computation 104(1):2-34, 1993 (preliminary version appeared in Proc. 5th LICS, 1990). Abstract. Full paper.
R. Alur and T.A. Henzinger. Real-time logics: complexity and expressiveness. Information and Computation 104(1):35-77, 1993 (preliminary version appeared in Proc. 5th LICS, 1990). Abstract. Full paper.

Back to the homepage of Rajeev Alur.