Travelled to:
1 × Canada
1 × Croatia
1 × Denmark
1 × Estonia
1 × Finland
1 × Hungary
1 × Iceland
1 × Japan
1 × Norway
1 × Russia
1 × Switzerland
1 × The Netherlands
2 × Austria
2 × Poland
2 × Portugal
2 × Spain
3 × France
3 × United Kingdom
6 × USA
Collaborated with:
J.Worrell A.S.Murawski ∅ C.Haase D.Kröning O.Strichman D.Bundala S.Kiefer B.Wachter E.M.Clarke H.Ho S.Göller M.Jenkins A.Rabinovich P.Bouyer N.Markey M.W.Mislove S.A.Seshia S.Chaki N.Sharygina A.Lechner P.Hunter V.Chonev S.Ishtiaq M.J.Parkinson A.Legay P.A.Abdulla J.Deneux D.Pavlovic F.v.Breugel T.Antonopoulos N.Gorogiannis M.I.Kanovich T.Wahl L.Zhang N.Sinha T.Brihaye L.Doyen G.Geeraerts J.Raskin R.E.Bryant B.A.Brady P.J.Armstrong M.Goldsmith G.Lowe H.Palikareva A.W.Roscoe O.Grumberg T.Touili H.Veith
Talks about:
time (11) automata (9) check (9) model (8) problem (7) logic (7) decid (7) complex (6) bound (6) probabilist (5)
Person: Joël Ouaknine
DBLP: Ouaknine:Jo=euml=l
Contributed to:
Wrote 40 papers:
- FoSSaCS-2015-HoO #problem
- The Cyclic-Routing UAV Problem is PSPACE-Complete (HMH, JO), pp. 328–342.
- LICS-2015-LechnerOW #complexity #linear #on the
- On the Complexity of Linear Arithmetic with Divisibility (AL, JO, JW), pp. 667–676.
- FoSSaCS-2014-AntonopoulosGHKO #induction #logic #problem
- Foundations for Decision Problems in Separation Logic with General Inductive Predicates (TA, NG, CH, MIK, JO), pp. 411–425.
- ICALP-v2-2014-BundalaO #complexity #on the
- On the Complexity of Temporal-Logic Path Checking (DB, JO), pp. 86–97.
- ICALP-v2-2014-OuaknineW #linear #on the #problem #sequence
- On the Positivity Problem for Simple Linear Recurrence Sequences, (JO, JW), pp. 318–329.
- ICALP-v2-2014-OuaknineW14a #decidability #linear #sequence
- Ultimate Positivity is Decidable for Simple Linear Recurrence Sequences (JO, JW), pp. 330–341.
- CAV-2013-HaaseIOP #graph #logic #named #reasoning
- SeLoger: A Tool for Graph-Based Reasoning in Separation Logic (CH, SI, JO, MJP), pp. 790–795.
- LATA-2013-Ouaknine #linear
- Discrete Linear Dynamical Systems (JO), p. 42.
- LICS-2013-HunterOW #logic #metric
- Expressive Completeness for Metric Temporal Logic (PH, JO, JW), pp. 349–357.
- STOC-2013-ChonevOW #problem
- The orbit problem in higher dimensions (VC, JO, JW), pp. 941–950.
- CAV-2012-ArmstrongGLOPRW
- Recent Developments in FDR (PJA, MG, GL, JO, HP, AWR, JW), pp. 699–704.
- CAV-2012-KieferMOWW #named #probability #source code
- APEX: An Analyzer for Open Probabilistic Programs (SK, ASM, JO, BW, JW), pp. 693–698.
- FoSSaCS-2012-GollerHOW #automaton #model checking #parametricity
- Branching-Time Model Checking of Parametric One-Counter Automata (SG, CH, JO, JW), pp. 406–420.
- FoSSaCS-2012-KieferMOWW #automaton #complexity #equivalence #on the #probability #problem
- On the Complexity of the Equivalence Problem for Probabilistic Automata (SK, ASM, JO, BW, JW), pp. 467–481.
- LICS-2012-BundalaOW #bound #model checking #on the
- On the Magnitude of Completeness Thresholds in Bounded Model Checking (DB, JO, JW), pp. 155–164.
- CAV-2011-KieferMOWW #automaton #equivalence #probability
- Language Equivalence for Probabilistic Automata (SK, ASM, JO, BW, JW), pp. 526–540.
- CAV-2011-KroeningOSWW #bound #linear #model checking
- Linear Completeness Thresholds for Bounded Model Checking (DK, JO, OS, TW, JW), pp. 557–572.
- CSL-2011-JenkinsORW #metric #problem #synthesis
- The Church Synthesis Problem with Metric (MJ, JO, AR, JW), pp. 307–321.
- ICALP-v2-2011-BrihayeDGORW #automaton #bound #hybrid #on the #reachability
- On Reachability for Hybrid Automata over Bounded Time (TB, LD, GG, JO, JFR, JW), pp. 416–427.
- ICALP-v2-2011-KieferMOWZ #algorithm #on the
- On Stabilization in Herman’s Algorithm (SK, ASM, JO, JW, LZ), pp. 466–477.
- ICALP-v2-2010-GollerHOW #automaton #model checking #parametricity
- Model Checking Succinct and Parametric One-Counter Automata (SG, CH, JO, JW), pp. 575–586.
- ICALP-v2-2010-OuaknineW #bound #formal method #towards #verification
- Towards a Theory of Time-Bounded Verification (JO, JW), pp. 22–37.
- LICS-2010-JenkinsORW #automaton #bound
- Alternating Timed Automata over Bounded Time (MJ, JO, AR, JW), pp. 60–69.
- ICALP-B-2008-BouyerMOW #complexity #model checking #on the #realtime
- On Expressiveness and Complexity in Real-Time Model Checking (PB, NM, JO, JW), pp. 124–135.
- TACAS-2008-LegayMOW #automation #on the #probability #source code #verification
- On Automated Verification of Probabilistic Programs (AL, ASM, JO, JW), pp. 173–187.
- LICS-2007-BouyerMOW #cost analysis
- The Cost of Punctuality (PB, NM, JO, JW), pp. 109–120.
- TACAS-2007-BryantKOSSB #abstraction
- Deciding Bit-Vector Arithmetic with Abstraction (REB, DK, JO, SAS, OS, BAB), pp. 358–372.
- FoSSaCS-2006-OuaknineW #logic #metric #on the #turing machine
- On Metric Temporal Logic and Faulty Turing Machines (JO, JW), pp. 217–230.
- TACAS-2006-OuaknineW #decidability #logic #metric #safety
- Safety Metric Temporal Logic Is Fully Decidable (JO, JW), pp. 411–425.
- ICALP-2005-AbdullaDOW #automaton #complexity #decidability
- Decidability and Complexity Results for Timed Automata via Channel Machines (PAA, JD, JO, JW), pp. 1089–1101.
- IFM-2005-ChakiCGOSTV #specification #verification
- State/Event Software Verification for Branching-Time Specifications (SC, EMC, OG, JO, NS, TT, HV), pp. 53–69.
- LICS-2005-OuaknineW #decidability #logic #metric #on the
- On the Decidability of Metric Temporal Logic (JO, JW), pp. 188–197.
- CAV-2004-KroeningOSS #satisfiability
- Abstraction-Based Satisfiability Solving of Presburger Arithmetic (DK, JO, SAS, OS), pp. 308–320.
- FoSSaCS-2004-MisloveOPW #markov #process
- Duality for Labelled Markov Processes (MWM, JO, DP, JW), pp. 393–407.
- IFM-2004-ChakiCOSS #model checking
- State/Event-Based Software Model Checking (SC, EMC, JO, NS, NS), pp. 128–147.
- LICS-2004-OuaknineW #automaton #decidability #on the #problem
- On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap (JO, JW), pp. 54–63.
- VMCAI-2004-ClarkeKOS #bound #complexity #model checking
- Completeness and Complexity of Bounded Model Checking (EMC, DK, JO, OS), pp. 85–96.
- FoSSaCS-2003-BreugelMOW #approximate #probability #similarity
- An Intrinsic Characterization of Approximate Probabilistic Bisimilarity (FvB, MWM, JO, JW), pp. 200–215.
- LICS-2003-OuaknineW #automaton #decidability #robust
- Revisiting Digitization, Robustness, and Decidability for Timed Automata (JO, JW), pp. 198–207.
- TACAS-2002-Ouaknine #abstraction #model checking
- Digitisation and Full Abstraction for Dense-Time Model Checking (JO), pp. 37–51.