Travelled to:1 × Austria
1 × Canada
1 × Estonia
1 × Finland
1 × Germany
1 × Greece
1 × Hungary
1 × Poland
1 × Russia
1 × Spain
14 × USA
2 × France
2 × Portugal
4 × Italy
5 × United Kingdom
Collaborated with:R.Alur G.Parlato A.Farzan P.Garg S.L.Torre ∅ X.Qiu D.Neider S.Chaudhuri F.Sorrentino C.Löding S.Saha U.Mathur M.V.0001 A.L.Ferrara M.Viswanathan W.Nam K.Etessami P.S.Thiagarajan D.D'Souza Pranav Garg 0001 A.Desai E.Pek R.Chadha R.K.Karmani B.M.Moore M.Bernadsky L.Peña T.L.Nguyen N.Razavi V.Kumar P.Cerný P.Bouyer A.Petit D.Roth P. Ezudheen A.Astorga Shiyu Wang T.X.0001 Adithya Murali Paul Krogmeier
Talks about:program (8) learn (8) concurr (6) structur (5) reachabl (5) atom (5) use (5) control (4) analysi (4) invari (4)
Person: P. Madhusudan
DBLP: Madhusudan:P=
Facilitated 1 volumes:
EdContributed to:
20152014
2014
20142013
2013
2013
20122012
2011
20112011201120102010200920092008
200820082007
20072006
200620062005
2005200520052004
2004
200420042003
2003200320012018201820162018201920192020Wrote 50 papers:
- CAV-2015-Saha0M #learning #named
- Alchemist: Learning Guarded Affine Functions (SS, PG, PM), pp. 440–446.
- CAV-2014-0001LMN #framework #invariant #learning #named #robust
- ICE: A Robust Framework for Learning Invariants (PG, CL, PM, DN), pp. 69–87.
- CAV-2014-FerraraMNP #data access #named #policy #verification
- Vac — Verifier of Administrative Role-Based Access Control Policies (ALF, PM, TLN, GP), pp. 184–191.
- OOPSLA-2014-Desai0M #proving #reduction #source code #using
- Natural proofs for asynchronous programs using almost-synchronous reductions (AD, PG, PM), pp. 709–725.
- PLDI-2014-PekQM #c #data type #logic #proving #using
- Natural proofs for data structure manipulation in C using separation logic (EP, XQ, PM), p. 46.
- CAV-2013-0001LMN #data type #invariant #learning #linear #quantifier
- Learning Universally Quantified Invariants of Linear Data Structures (PG, CL, PM, DN), pp. 813–829.
- SAS-2013-0001MP #abstract domain #automaton #quantifier
- Quantified Data Automata on Skinny Trees: An Abstract Domain for Lists (PG, PM, GP), pp. 172–193.
- TACAS-2013-FerraraMP #analysis #data access #policy #self
- Policy Analysis for Self-administrated Role-Based Access Control (ALF, PM, GP), pp. 432–447.
- FSE-2012-FarzanMRS #concurrent #predict #source code
- Predicting null-pointer dereferences in concurrent programs (AF, PM, NR, FS), p. 47.
- TACAS-2012-ChadhaMV #reachability
- Reachability under Contextual Locking (RC, PM, MV), pp. 437–450.
- POPL-2011-MadhusudanP
- The tree width of auxiliary storage (PM, GP), pp. 283–294.
- POPL-2011-MadhusudanPQ #decidability #logic
- Decidable logics combining heap structures and data (PM, GP, XQ), pp. 611–622.
- PPoPP-2011-KarmaniMM #concurrent #contract #parallel #thread
- Thread contracts for safe parallelism (RKK, PM, BMM), pp. 125–134.
- SAS-2011-MadhusudanQ #performance #using
- Efficient Decision Procedures for Heaps Using STRAND (PM, XQ), pp. 43–59.
- TACAS-2011-GargM #composition
- Compositionality Entails Sequentializability (PG, PM), pp. 26–40.
- CAV-2010-TorreMP #concurrent #interface #linear #model checking #source code #using
- Model-Checking Parameterized Concurrent Programs Using Linear Interfaces (SLT, PM, GP), pp. 629–644.
- FSE-2010-SorrentinoFM #named #thread #weaving
- PENELOPE: weaving threads to expose atomicity violations (FS, AF, PM), pp. 37–46.
- CAV-2009-FarzanMS
- Meta-analysis for Atomicity Violations under Nested Locking (AF, PM, FS), pp. 248–262.
- CAV-2009-TorreMP #bound #concurrent #reachability
- Reducing Context-Bounded Concurrent Reachability to Sequential Reachability (SLT, PM, GP), pp. 477–492.
- TACAS-2009-FarzanM #complexity #predict
- The Complexity of Predicting Atomicity Violations (AF, PM), pp. 155–169.
- CAV-2008-FarzanM #concurrent #monitoring #source code
- Monitoring Atomicity in Concurrent Programs (AF, PM), pp. 52–65.
- CSL-2008-TorreMP #automaton #exponential #infinity
- An Infinite Automaton Characterization of Double Exponential Time (SLT, PM, GP), pp. 33–48.
- TACAS-2008-TorreMP #analysis #bound #concurrent #queue
- Context-Bounded Analysis of Concurrent Queue Systems (SLT, PM, GP), pp. 299–314.
- TACAS-2007-FarzanM #analysis #concurrent #data flow #source code
- Causal Dataflow Analysis for Concurrent Programs (AF, PM), pp. 102–116.
- VMCAI-2007-Madhusudan #algorithm #learning #verification
- Learning Algorithms and Formal Verification (PM), p. 214.
- CAV-2006-AlurCM
- Languages of Nested Trees (RA, SC, PM), pp. 329–342.
- CAV-2006-FarzanM
- Causal Atomicity (AF, PM), pp. 315–328.
- DLT-2006-AlurM #word
- Adding Nesting Structure to Words (RA, PM), pp. 1–13.
- 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.
- 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.
- CAV-2003-BouyerDMP
- Timed Control with Partial Observability (PB, DD, PM, AP), pp. 180–192.
- LICS-2003-Madhusudan #model checking
- Model-checking Trace Event Structures (PM), pp. 371–380.
- TACAS-2003-AlurTM #composition #game studies #graph #recursion
- Modular Strategies for Recursive Game Graphs (RA, SLT, PM), pp. 363–378.
- ICALP-2001-Madhusudan #behaviour #branch #graph #reasoning #sequence
- Reasoning about Sequential and Branching Behaviours of Message Sequence Graphs (PM), pp. 809–820.
- ICALP-2001-MadhusudanT #distributed #specification #synthesis
- Distributed Controller Synthesis for Local Specifications (PM, PST), pp. 396–407.
- CSL-2018-MadhusudanMS0 #decidability #higher-order #logic #synthesis
- A Decidable Fragment of Second Order Logic With Applications to Synthesis (PM, UM, SS, MV0), p. 19.
- OOPSLA-2018-EzudheenND0M #contract #invariant #learning
- Horn-ICE learning for synthesizing invariants and contracts (PE, DN, DD, PG0, PM), p. 25.
- POPL-2016-0001NMR #invariant #learning #using
- Learning invariants using decision trees and implication counterexamples (PG0, DN, PM, DR), pp. 499–512.
- POPL-2018-LodingMP #proving #quantifier
- Foundations for natural proofs and quantifier instantiation (CL, PM, LP), p. 30.
- PLDI-2019-AstorgaMSWX #generative #learning
- Learning stateful preconditions modulo a test generator (AA, PM, SS, SW, TX0), pp. 775–787.
- POPL-2019-MathurMV #decidability #source code #verification
- Decidable verification of uninterpreted programs (UM, PM, MV0), p. 29.
- POPL-2020-MathurMKMV #memory management #safety #source code
- Deciding memory safety for single-pass heap-manipulating programs (UM, AM, PK, PM, MV0), p. 29.