Gregory Malecha

23 papers A 2B 1C 3Misc 2Journal 10Unranked 5
YearRankTypeTitle / Venue / Authors
2026 J jnl
Recursive Mutexes in Separation Logic.
CoRR
Ke Du, William Mansky, Paolo G. Giarrusso, Gregory Malecha
2025 A conf
Modular, Full-System Verification.
HotOS
Gregory Malecha, Hoang-Hai Dang, Paolo G. Giarrusso, Simon Hudon, Jan-Oliver Kaiser, David Swasey
2022 J jnl
Developing With Formal Methods at BedRock Systems, Inc.
IEEE Secur. Priv.
Gregory Malecha, Gordon Stewart, Frantisek Farka, Jasper Haag, Yoichi Hirai
2021 J jnl
Formal Methods for the Informal Engineer: Workshop Recommendations.
CoRR
Gopal Sarma, James Koppel, Gregory Malecha, Patrick Schultz, Eric Drexler, Ramana Kumar, Cody Roux, Philip Zucker
2020 J jnl
Interaction trees: representing recursive and impure programs in Coq.
Proc. ACM Program. Lang.
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
2020 J jnl
The MetaCoq Project.
J. Autom. Reason.
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter
2019 J jnl
Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress).
CoRR
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
2016 A conf
Extensible and Efficient Automation Through Reflective Tactics.
ESOP
Gregory Malecha, Jesper Bengtson
2016 Misc conf
Modular deductive verification of sampled-data systems.
EMSOFT
Daniel Ricketts, Gregory Malecha, Sorin Lerner
2016 — conf
Towards foundational verification of cyber-physical systems.
SOSCYPS@CPSWeek
Gregory Malecha, Daniel Ricketts, Mario M. Alvarez, Sorin Lerner
2015 Misc conf
Automated software winnowing.
SAC
Gregory Malecha, Ashish Gehani, Natarajan Shankar
2015 C conf
Towards verification of hybrid systems in a foundational proof assistant.
MEMOCODE
Daniel Ricketts, Gregory Malecha, Mario M. Alvarez, Vignesh Gowda, Sorin Lerner
2015 — conf
Using dependent types and tactics to enable semantic optimization of language-integrated queries.
DBPL
Gregory Malecha, Ryan Wisnesky
2014 B conf
Compositional Computational Reflection.
ITP
Gregory Malecha, Adam Chlipala, Thomas Braibant
2013 J jnl
MirrorShard: Proof by Computational Reflection with Verified Hints
CoRR
Gregory Malecha, Adam Chlipala, Thomas Braibant, Patrick Hulin, Edward Z. Yang
2012 — conf
Hardware Support for Safety Interlocks and Introspection.
SASO Workshops
Udit Dhawan, Albert Kwon, Edin Kadric, Catalin Hritcu, Benjamin C. Pierce, Jonathan M. Smith, André DeHon, Gregory Malecha, Greg Morrisett, Thomas F. Knight Jr., Andrew Sutherland, Tom Hawkins, Amanda Zyxnfryx, David K. Wittenberg, Peter Trei, Sumit Ray, Greg Sullivan
2011 — conf
Preliminary design of the SAFE platform.
PLOS@SOSP
André DeHon, Ben Karel, Thomas F. Knight Jr., Gregory Malecha, Benoît Montagu, Robin Morisset, Greg Morrisett, Benjamin C. Pierce, Randy Pollack, Sumit Ray, Olin Shivers, Jonathan M. Smith, Gregory Sullivan
2011 J jnl
Static consistency checking for Verilog wire interconnects - Using dependent types to check the sanity of Verilog descriptions.
High. Order Symb. Comput.
Cherif R. Salama, Gregory Malecha, Walid Taha, Jim Grundy, John O'Leary
2011 J jnl
Trace-based verification of imperative programs with I/O.
J. Symb. Comput.
Gregory Malecha, Greg Morrisett, Ryan Wisnesky
2010 — conf
A more precise security type system for dynamic security tests.
PLAS
Gregory Malecha, Stephen Chong
2010 J jnl
Synthesizable High Level Hardware Descriptions.
New Gener. Comput.
Jennifer Gillenwater, Gregory Malecha, Cherif R. Salama, Angela Yun Zhu, Walid Taha, Jim Grundy, John O'Leary
2009 C conf
Static consistency checking for verilog wire interconnects: using dependent types to check the sanity of verilog descriptions.
PEPM
Cherif R. Salama, Gregory Malecha, Walid Taha, Jim Grundy, John O'Leary
2008 C conf
Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee verilog synthesizability.
PEPM
Jennifer Gillenwater, Gregory Malecha, Cherif R. Salama, Angela Yun Zhu, Walid Taha, Jim Grundy, John O'Leary