Travelled to:
1 × Belgium
1 × China
1 × Croatia
1 × Czech Republic
1 × Estonia
1 × Finland
1 × Germany
1 × Ireland
1 × Israel
1 × Latvia
1 × Switzerland
2 × Austria
2 × Denmark
2 × Greece
2 × India
2 × Poland
28 × USA
3 × Italy
4 × Canada
4 × Portugal
4 × Spain
5 × France
6 × United Kingdom
Collaborated with:
P.Madhusudan T.A.Henzinger P.Cerný M.Yannakakis M.Raghothaman K.Etessami S.Chaudhuri M.M.K.Martin D.Peled L.D'Antoni ∅ R.Grosu S.L.Torre C.Courcoubetis D.L.Dill S.Burckhardt S.K.Rajamani S.Mador-Haim S.Moarref J.V.Deshmukh S.Kannan A.Kanade G.Weiss K.Mamouras F.Ivancic U.Topcu A.Trivedi M.McDougall K.L.McMillan B.Wang W.Nam A.Radhakrishna Caleb Stanford N.Singhania Y.Yuan I.Lee Z.G.Ives A.Udupa S.Qadeer A.Freilich A.Durand-Gasselin E.Filiot S.Weinstein S.Zdancewic M.Bernadsky T.Dang Z.Yang G.J.Holzmann W.Penczek L.Fix H.Attiya G.Taubenfeld M.Y.Vardi D.Fisman F.Y.C.Mang K.Tian G.Ramalingam A.Degorre O.Maler V.Kumar M.Viswanathan L.J.Jagadeesan J.J.Kott J.V.Olnhausen A.Itai R.P.Kurshan M.Faella J.Devietti O.S.N.Leija W.Lee K.Heo M.Naik C.Stergiou S.Tripakis Z.Jiang M.Pajic R.Mangharam D.Zufferey J.Kim O.Sokolsky J.M.Esposito M.Kim V.Kumar R.K.Brayton S.Khanna V.Tannen A.Raghavan A.D'Innocenzo A.J.Isaksson K.H.Johansson G.J.Pappas S.Ramesh S.Sankaranarayanan K.C.Shashidhar M.Arenas P.Barceló N.Immerman L.Libkin S.Tasiran L.d.Alfaro M.Kang C.M.Kirsch R.Majumdar L.Maranget S.Sarkar K.Memarian J.Alglave S.Owens P.Sewell D.Williams
Talks about:
model (25) check (15) time (13) system (11) program (9) automata (7) stream (7) machin (7) real (7) regular (6)
Person: Rajeev Alur
DBLP: Alur:Rajeev
Facilitated 2 volumes:
Contributed to:
Wrote 95 papers:
- CAV-2015-AlurCR #synthesis #unification
- Synthesis Through Unification (RA, PC, AR), pp. 163–179.
- CAV-2015-AlurRSTU #automation #distributed #protocol #symmetry
- Automatic Completion of Distributed Protocols with Symmetry (RA, MR, CS, ST, AU), pp. 395–412.
- POPL-2015-AlurDR #declarative #named #string
- DReX: A Declarative Language for Efficiently Evaluating Regular String Transformations (RA, LD, MR), pp. 125–137.
- TACAS-2015-AlurMT #refinement #specification #synthesis
- Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis (RA, SM, UT), pp. 501–516.
- CAV-2014-DAntoniA #automaton
- Symbolic Visibly Pushdown Automata (LD, RA), pp. 209–225.
- LICS-CSL-2014-AlurFR #combinator #string
- Regular combinators for string transformations (RA, AF, MR), p. 10.
- ICALP-v2-2013-AlurR #problem
- Decision Problems for Additive Regular Functions (RA, MR), pp. 37–48.
- LATA-2013-AlurKTY #complexity #graph #on the #problem
- On the Complexity of Shortest Path Problems on Discounted Cost Graphs (RA, SK, KT, YY), pp. 44–55.
- LICS-2013-AlurDDRY #automaton
- Regular Functions and Cost Register Automata (RA, LD, JVD, MR, YY), pp. 13–22.
- LICS-2013-AlurDT #higher-order #monad #string #transducer
- From Monadic Second-Order Definable String Transformations to Transducers (RA, ADG, AT), pp. 458–467.
- PLDI-2013-UdupaRDMMA #named #protocol #specification
- TRANSIT: specifying protocols with concolic snippets (AU, AR, JVD, SMH, MMKM, RA), pp. 287–296.
- CAV-2012-Mador-HaimMSMAOAMSW #axiom #memory management #multi
- An Axiomatic Memory Model for POWER Multiprocessors (SMH, LM, SS, KM, JA, SO, RA, MMKM, PS, DW), pp. 495–512.
- ICALP-v2-2012-AlurD #streaming #transducer
- Streaming Tree Transducers (RA, LD), pp. 42–53.
- LICS-2012-AlurFT #infinity #string
- Regular Transformations of Infinite Strings (RA, EF, AT), pp. 65–74.
- TACAS-2012-JiangPMAM #modelling #verification
- Modeling and Verification of a Dual Chamber Implantable Pacemaker (ZJ, MP, SM, RA, RM), pp. 188–203.
- DAC-2011-Mador-HaimAM #consistency #how #memory management #modelling #question #testing
- Litmus tests for comparing memory consistency models: how long do they need to be? (SMH, RA, MMKM), pp. 504–509.
- ICALP-v2-2011-AlurD #nondeterminism #streaming #string #transducer
- Nondeterministic Streaming String Transducers (RA, JVD), pp. 1–20.
- POPL-2011-AlurC #algorithm #source code #streaming #transducer #verification
- Streaming transducers for algorithmic verification of single-pass list-processing programs (RA, PC), pp. 599–610.
- CAV-2010-CernyRZCA #concurrent #implementation #model checking
- Model Checking of Linearizability of Concurrent List Implementations (PC, AR, DZ, SC, RA), pp. 465–479.
- CAV-2010-Mador-HaimAM #consistency #generative #memory management #modelling #testing
- Generating Litmus Tests for Contrasting Memory Consistency Models (SMH, RA, MMKM), pp. 273–287.
- FSE-2010-KanadeARR #dependence #representation #testing #using
- Representation dependence testing using program inversion (AK, RA, SKR, GR), pp. 277–286.
- VMCAI-2010-AlurC #reasoning #source code
- Temporal Reasoning for Procedural Programs (RA, SC), pp. 45–60.
- CASE-2009-DInnocenzoWAIJP #algorithm #scalability #scheduling
- Scalable scheduling algorithms for wireless networked control systems (AD, GW, RA, AJI, KHJ, GJP), pp. 409–414.
- CAV-2009-CernyA #analysis #automation #java
- Automated Analysis of Java Methods for Confidentiality (PC, RA), pp. 173–187.
- CAV-2009-KanadeAIRSS #generative #modelling
- Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models (AK, RA, FI, SR, SS, KCS), pp. 430–445.
- CSL-2009-AlurCW #algorithm #analysis #source code
- Algorithmic Analysis of Array-Accessing Programs (RA, PC, SW), pp. 86–101.
- FoSSaCS-2009-Alur #reasoning
- Temporal Reasoning about Program Executions (RA), p. 15.
- FoSSaCS-2009-AlurDMW #on the
- On ω-Languages Defined by Mean-Payoff Conditions (RA, AD, OM, GW), pp. 333–347.
- CAV-2008-AlurKW #automaton #game studies #ranking #requirements
- Ranking Automata and Games for Prioritized Requirements (RA, AK, GW), pp. 240–253.
- LICS-2007-AlurABEIL #first-order #logic #word
- First-Order and Temporal Logics for Nested Words (RA, MA, PB, KE, NI, LL), pp. 151–160.
- PLDI-2007-BurckhardtAM #concurrent #consistency #data type #memory management #modelling #named
- CheckFence: checking consistency of concurrent data types on relaxed memory models (SB, RA, MMKM), pp. 12–21.
- PODS-2007-Alur #word
- Marrying words and trees (RA), pp. 233–242.
- TACAS-2007-AlurCC #model checking
- Model Checking on Trees with Path Equivalences (RA, PC, SC), pp. 664–678.
- CAV-2006-AlurCM
- Languages of Nested Trees (RA, SC, PM), pp. 329–342.
- CAV-2006-BurckhardtAM #bound #case study #concurrent #data type #memory management #model checking #modelling
- Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study (SB, RA, MMKM), pp. 489–502.
- DLT-2006-AlurM #word
- Adding Nesting Structure to Words (RA, PM), pp. 1–13.
- ICALP-v2-2006-AlurCZ #refinement
- Preserving Secrecy Under Refinement (RA, PC, SZ), pp. 107–118.
- POPL-2006-AlurCM #calculus #fixpoint
- A fixpoint calculus for local and global program flows (RA, SC, PM), pp. 153–165.
- CAV-2005-AlurMN #composition #learning #verification
- Symbolic Compositional Verification by Learning Assumptions (RA, PM, WN), pp. 548–562.
- ICALP-2005-AlurKMV #automaton
- Congruences for Visibly Pushdown Languages (RA, VK, PM, MV), pp. 1102–1114.
- POPL-2005-AlurCMN #interface #java #specification #synthesis
- Synthesis of interface specifications for Java classes (RA, PC, PM, WN), pp. 98–109.
- TACAS-2005-AlurCEM #detection #on the fly #reachability #recursion #state machine
- On-the-Fly Reachability and Cycle Detection for Recursive State Machines (RA, SC, KE, PM), pp. 61–76.
- VMCAI-2005-BurckhardtAM #composition #implementation #parametricity #refinement #safety #verification
- Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement (SB, RA, MMKM), pp. 130–145.
- ICALP-2004-AlurBM #game studies #reachability
- Optimal Reachability for Weighted Timed Games (RA, MB, PM), pp. 122–133.
- SFM-2004-AlurM #automaton #overview #problem
- Decision Problems for Timed Automata: A Survey (RA, PM), pp. 1–24.
- STOC-2004-AlurM #automaton
- Visibly pushdown languages (RA, PM), pp. 202–211.
- TACAS-2004-AlurEM #logic
- A Temporal Logic of Nested Calls and Returns (RA, KE, PM), pp. 467–481.
- CAV-2003-AlurTM #composition #game studies #graph #infinity #recursion
- Modular Strategies for Infinite Games on Recursive Graphs (RA, SLT, PM), pp. 67–79.
- LCTES-2003-AlurIKLS #embedded #generative #hybrid #modelling
- Generating embedded software from hierarchical hybrid models (RA, FI, JK, IL, OS), pp. 171–182.
- TACAS-2003-AlurDI #abstraction #hybrid
- Counter-Example Guided Predicate Abstraction of Hybrid Systems (RA, TD, FI), pp. 208–223.
- TACAS-2003-AlurTM #composition #game studies #graph #recursion
- Modular Strategies for Recursive Game Graphs (RA, SLT, PM), pp. 363–378.
- CAV-2002-AlurMY #behaviour #model checking #performance
- Exploiting Behavioral Hierarchy for Efficient Model Checking (RA, MM, ZY), pp. 338–342.
- ASE-2001-AlurG #diagrams #interactive
- Shared Variables Interaction Diagrams (RA, RG), pp. 281–288.
- CAV-2001-AlurEY #analysis #recursion #state machine
- Analysis of Recursive State Machines (RA, KE, MY), pp. 207–220.
- CAV-2001-AlurW #implementation #network #protocol #refinement #verification
- Verifying Network Protocol Implementations by Symbolic Refinement Checking (RA, BYW), pp. 169–181.
- ICALP-2001-AlurEY #graph #verification
- Realizability and Verification of MSC Graphs (RA, KE, MY), pp. 797–808.
- ICSE-2001-AlurAGHKKMMW #design #model checking #named
- JMOCHA: A Model Checking Tool that Exploits Design Structure (RA, LdA, RG, TAH, MK, CMK, RM, FYCM, BYW), pp. 835–836.
- LICS-2001-AlurT #game studies #generative #ltl
- Deterministic Generators and Games for LTL Fragments (RA, SLT), pp. 291–300.
- CAV-2000-AlurGM #analysis #performance #reachability
- Efficient Reachability Analysis of Hierarchical Reactive Machines (RA, RG, MM), pp. 280–295.
- ICSE-2000-AlurEY #sequence chart
- Inference of message sequence charts (RA, KE, MY), pp. 304–313.
- POPL-2000-AlurG #composition #refinement
- Modular Refinement of Hierarchic Reactive Machines (RA, RG), pp. 390–402.
- CAV-1999-Alur #automaton
- Timed Automata (RA), pp. 8–22.
- FM-v1-1999-AlurEKKL #analysis #case study #coordination #formal method #hybrid #modelling #multi
- Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination (RA, JME, MK, VK, IL), pp. 212–232.
- ICALP-1999-AlurKY #communication #state machine
- Communicating Hierarchical State Machines (RA, SK, MY), pp. 169–178.
- ICALP-1999-AlurTEP #logic #parametricity
- Parametric Temporal Logic for “Model Measuring” (RA, KE, SLT, DP), pp. 159–168.
- CAV-1998-AlurHMQRT #composition #model checking #named
- MOCHA: Modularity in Model Checking (RA, TAH, FYCM, SQ, SKR, ST), pp. 521–525.
- FSE-1998-AlurY #model checking #state machine
- Model Checking of Hierarchical State Machines (RA, MY), pp. 175–188.
- ICALP-1998-AlurMP #partial order
- Deciding Global Partial-Order Properties (RA, KLM, DP), pp. 41–52.
- TACAS-1998-AlurHR
- Symbolic Exploration of transition Hierarchies (RA, TAH, SKR), pp. 330–344.
- CAV-1997-AlurBHQR #partial order #reduction
- Partial-Order Reduction in Symbolic State Space Exploration (RA, RKB, TAH, SQ, SKR), pp. 340–351.
- ICSE-1997-AlurJKO #model checking #realtime
- Model-Checking of Real-Time Systems: A Telecommunications Application (RA, LJJ, JJK, JVO), pp. 514–524.
- LICS-1996-AlurH
- Reactive Modules (RA, TAH), pp. 207–218.
- LICS-1996-AlurMP #concurrent #correctness #model checking
- Model-Checking of Correctness Conditions for Concurrent Objects (RA, KLM, DP), pp. 219–228.
- TACAS-1996-AlurHP #sequence chart
- An Analyser for Mesage Sequence Charts (RA, GJH, DP), pp. 35–48.
- CAV-1995-AlurH #composition #liveness #modelling
- Local Liveness for Compositional Modeling of Fair Reactive Systems (RA, TAH), pp. 166–179.
- LICS-1995-AlurPP #model checking
- Model-Checking of Causality Properties (RA, DP, WP), pp. 90–100.
- STOC-1995-AlurCY #nondeterminism #probability #testing
- Distinguishing tests for nondeterministic and probabilistic machines (RA, CC, MY), pp. 363–372.
- CAV-1994-AlurFH #automaton
- A Determinizable Class of Timed Automata (RA, LF, TAH), pp. 1–13.
- LICS-1994-AlurH
- Finitary Fairness (RA, TAH), pp. 52–61.
- STOC-1994-AlurAT #adaptation #algorithm
- Time-adaptive algorithms for synchronization (RA, HA, GT), pp. 800–809.
- CAV-1993-AlurCH #realtime
- Computing Accumulated Delays in Real-time Systems (RA, CC, TAH), pp. 181–193.
- STOC-1993-AlurHV #parametricity #realtime #reasoning
- Parametric real-time reasoning (RA, TAH, MYV), pp. 592–601.
- CAV-1992-AlurIKY #approximate #verification
- Timing Verification by Successive Approximation (RA, AI, RPK, MY), pp. 137–150.
- ICALP-1991-AlurCD #model checking #probability #realtime
- Model-Checking for Probabilistic Real-Time Systems (RA, CC, DLD), pp. 115–126.
- ICALP-1990-AlurD #automaton #modelling #realtime
- Automata For Modeling Real-Time Systems (RA, DLD), pp. 322–335.
- LICS-1990-AlurCD #model checking #realtime
- Model-Checking for Real-Time Systems (RA, CC, DLD), pp. 414–425.
- LICS-1990-AlurH #complexity #logic #realtime
- Real-time Logics: Complexity and Expressiveness (RA, TAH), pp. 390–401.
- ESOP-2016-AlurFR #data type #programming
- Regular Programming for Quantitative Properties of Data Streams (RA, DF, MR), pp. 15–40.
- CAV-2016-AlurMT #composition #multi #synthesis
- Compositional Synthesis of Reactive Controllers for Multi-agent Systems (RA, SM, UT), pp. 251–269.
- CSL-2016-AlurFKS #markov #process
- Hedging Bets in Markov Decision Processes (RA, MF, SK, NS), p. 20.
- CAV-2017-AlurDLS #detection #gpu #named #source code
- GPUDrano: Detecting Uncoalesced Accesses in GPU Programs (RA, JD, OSNL, NS), pp. 507–525.
- PLDI-2017-MamourasRAIK #composition #evaluation #named #performance #query #specification #streaming
- StreamQRE: modular specification and efficient evaluation of quantitative queries over streaming data (KM, MR, RA, ZGI, SK), pp. 693–708.
- PLDI-2018-LeeHAN #modelling #probability #search-based #synthesis #using
- Accelerating search-based program synthesis using learned probabilistic models (WL, KH, RA, MN), pp. 436–449.
- PLDI-2019-MamourasSAIT #distributed
- Data-trace types for distributed stream processing systems (KM, CS, RA, ZGI, VT), pp. 670–685.
- POPL-2019-AlurMS #composition #monitoring
- Modular quantitative monitoring (RA, KM, CS), p. 31.