Gregory Malecha

Publication Activity (10 Years)

Years Active: 2008-2022
Publications (10 Years): 8

Top Topics

Top Venues

Proc. ACM Program. Lang.

Publications

Gregory Malecha, Gordon Stewart, Frantisek Farka, Jasper Haag, Yoichi Hirai
Developing With Formal Methods at BedRock Systems, Inc. IEEE Secur. Priv. 20 (3) (2022)
Gopal Sarma, James Koppel, Gregory Malecha, Patrick Schultz, Eric Drexler, Ramana Kumar, Cody Roux, Philip Zucker
Formal Methods for the Informal Engineer: Workshop Recommendations. CoRR (2021)
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. 4 (POPL) (2020)
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter
The MetaCoq Project. J. Autom. Reason. 64 (5) (2020)
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress). CoRR (2019)
Gregory Malecha, Daniel Ricketts, Mario M. Alvarez, Sorin Lerner
Towards foundational verification of cyber-physical systems. SOSCYPS@CPSWeek (2016)
Daniel Ricketts, Gregory Malecha, Sorin Lerner
Modular deductive verification of sampled-data systems. EMSOFT (2016)
Gregory Malecha, Jesper Bengtson
Extensible and Efficient Automation Through Reflective Tactics. ESOP (2016)
Gregory Malecha, Ashish Gehani, Natarajan Shankar
Automated software winnowing. SAC (2015)
Daniel Ricketts, Gregory Malecha, Mario M. Alvarez, Vignesh Gowda, Sorin Lerner
Towards verification of hybrid systems in a foundational proof assistant. MEMOCODE (2015)
Gregory Malecha, Ryan Wisnesky
Using dependent types and tactics to enable semantic optimization of language-integrated queries. DBPL (2015)
Gregory Malecha, Adam Chlipala, Thomas Braibant
Compositional Computational Reflection. ITP (2014)
Gregory Malecha, Adam Chlipala, Thomas Braibant, Patrick Hulin, Edward Z. Yang
MirrorShard: Proof by Computational Reflection with Verified Hints CoRR (2013)
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
Hardware Support for Safety Interlocks and Introspection. SASO Workshops (2012)
Gregory Malecha, Greg Morrisett, Ryan Wisnesky
Trace-based verification of imperative programs with I/O. J. Symb. Comput. 46 (2) (2011)
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
Preliminary design of the SAFE platform. PLOS@SOSP (2011)
Cherif R. Salama, Gregory Malecha, Walid Taha, Jim Grundy, John O'Leary
Static consistency checking for Verilog wire interconnects - Using dependent types to check the sanity of Verilog descriptions. High. Order Symb. Comput. 24 (1-2) (2011)
Jennifer Gillenwater, Gregory Malecha, Cherif R. Salama, Angela Yun Zhu, Walid Taha, Jim Grundy, John O'Leary
Synthesizable High Level Hardware Descriptions. New Gener. Comput. 28 (4) (2010)
Gregory Malecha, Stephen Chong
A more precise security type system for dynamic security tests. PLAS (2010)
Cherif R. Salama, Gregory Malecha, Walid Taha, Jim Grundy, John O'Leary
Static consistency checking for verilog wire interconnects: using dependent types to check the sanity of verilog descriptions. PEPM (2009)
Jennifer Gillenwater, Gregory Malecha, Cherif R. Salama, Angela Yun Zhu, Walid Taha, Jim Grundy, John O'Leary
Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee verilog synthesizability. PEPM (2008)