Simple characterization of functionally complete one-element sets of propositional connectives. - Petar Maksimovic 001; Predrag Janicic (Math. Log. Q., 2006)

An Extension and Cooperation Mechanism for Heterogeneous Overlay Networks. - Vincenzo Ciancaglini; Luigi Liquori; Giang Ngo Hoang; Petar Maksimovic 001 (Networking Workshops, 2012)

A backward-compatible protocol for inter-routing over heterogeneous overlay networks. - Giang Ngo Hoang; Luigi Liquori; Vincenzo Ciancaglini; Petar Maksimovic 001; Hung Nguyen Chan (SAC, 2013)

HOCore in Coq. - Petar Maksimovic 001; Alan Schmitt (ITP, 2015)

Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks. - Furio Honsell; Luigi Liquori; Petar Maksimovic 001; Ivan Scagnetto (LFMTP, 2015)

First steps towards probabilistic justification logic. - Ioannis Kokkinis; Petar Maksimovic 001; Zoran Ognjanovic; Thomas Studer (Log. J. IGPL, 2015)

Analyzing the exhaustiveness of the Synapse protocol. - Bojan Marinkovic; Vincenzo Ciancaglini; Zoran Ognjanovic; Paola Glavan; Luigi Liquori; Petar Maksimovic 001 (Peer-to-Peer Netw. Appl., 2015)

An open logical framework. - Furio Honsell; Marina Lenisa; Ivan Scagnetto; Luigi Liquori; Petar Maksimovic 001 (J. Log. Comput., 2016)

Towards Logic-Based Verification of JavaScript Programs. - José Fragoso Santos; Philippa Gardner; Petar Maksimovic 001; Daiva Naudziuniene (CADE, 2017)

LLF𝒫: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads. - Furio Honsell; Luigi Liquori; Petar Maksimovic 001; Ivan Scagnetto (Log. Methods Comput. Sci., 2017)

Symbolic Execution for JavaScript. - José Fragoso Santos; Petar Maksimovic 001; Théotime Grohens; Julian Dolby; Philippa Gardner (PPDP, 2018)

Plugging-in proof development environments using Locks in LF. - Furio Honsell; Luigi Liquori; Petar Maksimovic 001; Ivan Scagnetto (Math. Struct. Comput. Sci., 2018)

JaVerT: JavaScript verification toolchain. - José Fragoso Santos; Petar Maksimovic 001; Daiva Naudziuniene; Thomas Wood 001; Philippa Gardner (Proc. ACM Program. Lang., 2018)

A Program Logic for First-Order Encapsulated WebAssembly. - Conrad Watt; Petar Maksimovic 001; Neelakantan R. Krishnaswami; Philippa Gardner (ECOOP, 2019)

JaVerT 2.0: compositional symbolic execution for JavaScript. - José Fragoso Santos; Petar Maksimovic 001; Gabriela Cunha Sampaio; Philippa Gardner (Proc. ACM Program. Lang., 2019)

A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications. - Gabriela Sampaio; José Fragoso Santos; Petar Maksimovic 001; Philippa Gardner (ECOOP, 2020)

Gillian, part i: a multi-language platform for symbolic execution. - José Fragoso Santos; Petar Maksimovic 001; Sacha-Élie Ayoun; Philippa Gardner (PLDI, 2020)

Gillian: Compositional Symbolic Execution for All. - José Fragoso Santos; Petar Maksimovic 001; Sacha-Élie Ayoun; Philippa Gardner (CoRR, 2020)

A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact). - Gabriela Sampaio; José Fragoso Santos; Petar Maksimovic 001; Philippa Gardner (Dagstuhl Artifacts Ser., 2020)

Gillian, Part II: Real-World Verification for JavaScript and C. - Petar Maksimovic 001; Sacha-Élie Ayoun; José Fragoso Santos; Philippa Gardner (CAV (2), 2021)

Gillian: A Multi-Language Platform for Unified Symbolic Analysis. - Petar Maksimovic 001; José Fragoso Santos; Sacha-Élie Ayoun; Philippa Gardner (CoRR, 2021)

Exact Separation Logic. - Petar Maksimovic 001; Caroline Cronjäger; Julian Sutherland; Andreas Lööw; Sacha-Élie Ayoun; Philippa Gardner (CoRR, 2022)

Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding. - Petar Maksimovic 001; Caroline Cronjäger; Andreas Lööw; Julian Sutherland; Philippa Gardner (ECOOP, 2023)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Caroline Cronjäger; Petar Maksimovic 001; Philippa Gardner (ECOOP, 2024)

Matching Plans for Frame Inference in Compositional Reasoning. - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Petar Maksimovic 001; Philippa Gardner (ECOOP, 2024)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version). - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Caroline Cronjäger; Petar Maksimovic 001; Philippa Gardner (CoRR, 2024)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact). - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Caroline Cronjäger; Nat Karmios; Petar Maksimovic 001; Philippa Gardner (Dagstuhl Artifacts Ser., 2024)

A Hybrid Approach to Semi-automated Rust Verification. - Sacha-Élie Ayoun; Xavier Denis; Petar Maksimovic 001; Philippa Gardner (Proc. ACM Program. Lang., 2025)