P. Madhusudan

Orcid: 0000-0002-9782-721X

Affiliations:
  • University of Illinois, USA


According to our database1, P. Madhusudan authored at least 115 papers between 1998 and 2023.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
Complete First-Order Reasoning for Properties of Functional Programs.
Proc. ACM Program. Lang., October, 2023

Perception Contracts for Safety of ML-Enabled Systems.
Proc. ACM Program. Lang., October, 2023

A First-order Logic with Frames.
ACM Trans. Program. Lang. Syst., June, 2023

Languages with Decidable Learning: A Meta-theorem.
Proc. ACM Program. Lang., April, 2023

2022
Model-guided synthesis of inductive lemmas for FOL with least fixpoints.
Proc. ACM Program. Lang., 2022

Learning formulas in finite variable logics.
Proc. ACM Program. Lang., 2022

Synthesizing axiomatizations using logic learning.
Proc. ACM Program. Lang., 2022

Composing Neural Learning and Symbolic Reasoning with an Application to Visual Discrimination.
Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, 2022

2021
Synthesizing contracts correct modulo a test generator.
Proc. ACM Program. Lang., 2021

2020
Deciding memory safety for single-pass heap-manipulating programs.
Proc. ACM Program. Lang., 2020

A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines.
J. Autom. Reason., 2020

Synthesizing Lemmas for Inductive Reasoning.
CoRR, 2020

What's Decidable About Program Verification Modulo Axioms?
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Decidable Synthesis of Programs with Uninterpreted Functions.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019
Decidable verification of uninterpreted programs.
Proc. ACM Program. Lang., 2019

Augmenting Neural Nets with Symbolic Synthesis: Applications to Few-Shot Learning.
CoRR, 2019

Deciding Memory Safety for Forest Datastructures.
CoRR, 2019

Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants.
Proceedings of the Static Analysis - 26th International Symposium, 2019

Learning stateful preconditions modulo a test generator.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Reachability in Concurrent Uninterpreted Programs.
Proceedings of the 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2019

Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity.
Proceedings of the 2019 Formal Methods in Computer Aided Design, 2019

2018
Compositional Synthesis of Piece-Wise Functions by Learning Classifiers.
ACM Trans. Comput. Log., 2018

Foundations for natural proofs and quantifier instantiation.
Proc. ACM Program. Lang., 2018

Horn-ICE learning for synthesizing invariants and contracts.
Proc. ACM Program. Lang., 2018

Invariant Synthesis for Incomplete Verification Engines.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Lagrange's Theorem for Binary Squares.
Proceedings of the 43rd International Symposium on Mathematical Foundations of Computer Science, 2018

A Decidable Fragment of Second Order Logic With Applications to Synthesis.
Proceedings of the 27th EACSL Annual Conference on Computer Science Logic, 2018

2017
Inferring Formal Properties of Production Key-Value Stores.
CoRR, 2017

Efficient Incrementalized Runtime Checking of Linear Measures on Lists.
Proceedings of the 2017 IEEE International Conference on Software Testing, 2017

2016
Synthesizing Piece-Wise Functions by Learning Classifiers.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Abstract Learning Frameworks for Synthesis.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Learning invariants using decision trees and implication counterexamples.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

2015

Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists.
Formal Methods Syst. Des., 2015

NetGen: synthesizing data-plane configurations for network policies.
Proceedings of the 1st ACM SIGCOMM Symposium on Software Defined Networking Research, 2015

Alchemist: Learning Guarded Affine Functions.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014
Security analysis for temporal role based access control.
J. Comput. Secur., 2014

Natural proofs for data structure manipulation in C using separation logic.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

Explicit and symbolic techniques for fast and scalable points-to analysis.
Proceedings of the 3rd ACM SIGPLAN International Workshop on the State Of the Art in Java Program analysis, 2014

Natural proofs for asynchronous programs using almost-synchronous reductions.
Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, 2014

Online learning versus blended learning: an exploratory study.
Proceedings of the First (2014) ACM Conference on Learning @ Scale, 2014

Vac - Verifier of Administrative Role-Based Access Control Policies.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

ICE: A Robust Framework for Learning Invariants.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013
Reachability under Contextual Locking.
Log. Methods Comput. Sci., 2013

Policy Analysis for Self-administrated Role-Based Access Control.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Quantified Data Automata on Skinny Trees: An Abstract Domain for Lists.
Proceedings of the Static Analysis - 20th International Symposium, 2013

Natural proofs for structure, data, and separation.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

Learning Universally Quantified Invariants of Linear Data Structures.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Verifying security invariants in ExpressOS.
Proceedings of the Architectural Support for Programming Languages and Operating Systems, 2013

2012
Sequentializing Parameterized Programs
Proceedings of the Proceedings Fourth Workshop on Foundations of Interface Technologies, 2012

Reachability under Contextual Locking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Predicting null-pointer dereferences in concurrent programs.
Proceedings of the 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), 2012

Analyzing temporal role based access control models.
Proceedings of the 17th ACM Symposium on Access Control Models and Technologies, 2012

Recursive proofs for inductive tree data-structures.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Automated Reasoning and Natural Proofs for Programs Manipulating Data Structures.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2012

Security Analysis of Role-Based Access Control through Program Verification.
Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

2011
Software model checking using languages of nested trees.
ACM Trans. Program. Lang. Syst., 2011

Vetting browser extensions for security vulnerabilities with VEX.
Commun. ACM, 2011

Compositionality Entails Sequentializability.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Efficient Decision Procedures for Heaps Using STRAND.
Proceedings of the Static Analysis - 18th International Symposium, 2011

Thread contracts for safe parallelism.
Proceedings of the 16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2011

Decidable logics combining heap structures and data.
Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

The tree width of auxiliary storage.
Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Synthesizing Reactive Programs.
Proceedings of the Computer Science Logic, 2011

2010
CANDID: Dynamic candidate evaluations for automatic prevention of SQL injection attacks.
ACM Trans. Inf. Syst. Secur., 2010

VEX: Vetting Browser Extensions for Security Vulnerabilities.
Proceedings of the 19th USENIX Security Symposium, 2010

PENELOPE: weaving threads to expose atomicity violations.
Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010

The Language Theory of Bounded Context-Switching.
Proceedings of the LATIN 2010: Theoretical Informatics, 2010

Model-Checking Parameterized Concurrent Programs Using Linear Interfaces.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009
Adding nesting structure to words.
J. ACM, 2009

The Complexity of Predicting Atomicity Violations.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Analyzing recursive programs using a fixed-point calculus.
Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009

Query Automata for Nested Words.
Proceedings of the Mathematical Foundations of Computer Science 2009, 2009

Reducing Context-Bounded Concurrent Reachability to Sequential Reachability.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Meta-analysis for Atomicity Violations under Nested Locking.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008
Automatic symbolic compositional verification by learning assumptions.
Formal Methods Syst. Des., 2008

Context-Bounded Analysis of Concurrent Queue Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

An Infinite Automaton Characterization of Double Exponential Time.
Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

A formal framework for reflective database access control policies.
Proceedings of the 2008 ACM Conference on Computer and Communications Security, 2008

Monitoring Atomicity in Concurrent Programs.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007
Visibly pushdown automata for streaming XML.
Proceedings of the 16th International Conference on World Wide Web, 2007

Learning Algorithms and Formal Verification (Invited Tutorial).
Proceedings of the Verification, 2007

Causal Dataflow Analysis for Concurrent Programs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

A Robust Class of Context-Sensitive Languages.
Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007

CANDID: preventing sql injection attacks using dynamic candidate evaluations.
Proceedings of the 2007 ACM Conference on Computer and Communications Security, 2007

2006
Modular strategies for recursive game graphs.
Theor. Comput. Sci., 2006

A fixpoint calculus for local and global program flows.
Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

Minimization, Learning, and Conformance Testing of Boolean Programs.
Proceedings of the CONCUR 2006 - Concurrency Theory, 17th International Conference, 2006

Causal Atomicity.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Languages of Nested Trees.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005
On-the-Fly Reachability and Cycle Detection for Recursive State Machines.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Synthesis of interface specifications for Java classes.
Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

Congruences for Visibly Pushdown Languages.
Proceedings of the Automata, Languages and Programming, 32nd International Colloquium, 2005

Perturbed Timed Automata.
Proceedings of the Hybrid Systems: Computation and Control, 8th International Workshop, 2005

The MSO Theory of Connectedly Communicating Processes.
Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005

Symbolic Compositional Verification by Learning Assumptions.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004
A Temporal Logic of Nested Calls and Returns.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Visibly pushdown languages.
Proceedings of the 36th Annual ACM Symposium on Theory of Computing, 2004

Decision Problems for Timed Automata: A Survey.
Proceedings of the Formal Methods for the Design of Real-Time Systems, 2004

Optimal Reachability for Weighted Timed Games.
Proceedings of the Automata, Languages and Programming: 31st International Colloquium, 2004

Visibly Pushdown Games.
Proceedings of the FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 2004

2003
Symbolic computational techniques for solving games.
Proceedings of the First International Workshop on Bounded Model Checking, 2003

Model-checking Trace Event Structures.
Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

Playing Games with Boxes and Diamonds.
Proceedings of the CONCUR 2003, 2003

Timed Control with Partial Observability.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

Modular Strategies for Infinite Games on Recursive Graphs.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002
Branching time controllers for discrete event systems.
Theor. Comput. Sci., 2002

Timed Control Synthesis for External Specifications.
Proceedings of the STACS 2002, 19th Annual Symposium on Theoretical Aspects of Computer Science, Antibes, 2002

Dynamic Message Sequence Charts.
Proceedings of the FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 2002

A Decidable Class of Asynchronous Distributed Controllers.
Proceedings of the CONCUR 2002, 2002

2001
Distributed Controller Synthesis for Local Specifications.
Proceedings of the Automata, Languages and Programming, 28th International Colloquium, 2001

Reasoning about Sequential and Branching Behaviours of Message Sequence Graphs.
Proceedings of the Automata, Languages and Programming, 28th International Colloquium, 2001

Beyond Message Sequence Graphs.
Proceedings of the FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 2001

2000
Open Systems in Reactive Environments: Control and Synthesis.
Proceedings of the CONCUR 2000, 2000

1998
Controllers for Discrete Event Systems via Morphisms.
Proceedings of the CONCUR '98: Concurrency Theory, 1998


  Loading...