BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Alur:Rajeev

Facilitated 2 volumes:

CAV 2004Ed
CAV 1996Ed

Contributed to:

CAV 20152015
POPL 20152015
TACAS 20152015
CAV 20142014
CSL-LICS 20142014
ICALP (2) 20132013
LATA 20132013
LICS 20132013
PLDI 20132013
CAV 20122012
ICALP (2) 20122012
LICS 20122012
TACAS 20122012
DAC 20112011
ICALP (2) 20112011
POPL 20112011
CAV 20102010
FSE 20102010
VMCAI 20102010
CASE 20092009
CAV 20092009
CSL 20092009
FOSSACS 20092009
CAV 20082008
LICS 20072007
PLDI 20072007
PODS 20072007
TACAS 20072007
CAV 20062006
DLT 20062006
ICALP (2) 20062006
POPL 20062006
CAV 20052005
ICALP 20052005
POPL 20052005
TACAS 20052005
VMCAI 20052005
ICALP 20042004
SFM-RT 20042004
STOC 20042004
TACAS 20042004
CAV 20032003
LCTES 20032003
TACAS 20032003
CAV 20022002
ASE 20012001
CAV 20012001
ICALP 20012001
ICSE 20012001
LICS 20012001
CAV 20002000
ICSE 20002000
POPL 20002000
CAV 19991999
World Congress on Formal Methods 19991999
ICALP 19991999
CAV 19981998
FSE 19981998
ICALP 19981998
TACAS 19981998
CAV 19971997
ICSE 19971997
LICS 19961996
TACAS 19961996
CAV 19951995
LICS 19951995
STOC 19951995
CAV 19941994
LICS 19941994
STOC 19941994
CAV 19931993
STOC 19931993
CAV 19921992
ICALP 19911991
ICALP 19901990
LICS 19901990
ESOP 20162016
CAV (2) 20162016
CSL 20162016
CAV (1) 20172017
PLDI 20172017
PLDI 20182018
PLDI 20192019
POPL 20192019

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.