The analysis of cyclic circuits with Boolean satisfiability. - John D. Backes; Brian Fett; Marc D. Riedel (ICCAD, 2008)

The Synthesis of Stochastic Circuits for Nanoscale Computation. - Weikang Qian; John D. Backes; Marc D. Riedel (Int. J. Nanotechnol. Mol. Comput., 2009)

Reduction of interpolants for logic synthesis. - John D. Backes; Marc D. Riedel (ICCAD, 2010)

The Synthesis of Cyclic Dependencies with Boolean Satisfiability. - John D. Backes; Marc D. Riedel (ACM Trans. Design Autom. Electr. Syst., 2012)

Using cubes of non-state variables with property directed reachability. - John D. Backes; Marc D. Riedel (DATE, 2013)

Ghost Talk: Mitigating EMI Signal Injection Attacks against Analog Sensors. - Denis Foo Kune; John D. Backes; Shane S. Clark; Daniel B. Kramer; Matthew R. Reynolds; Kevin Fu; Yongdae Kim; Wenyuan Xu 001 (IEEE Symposium on Security and Privacy, 2013)

Regression Verification Using Impact Summaries. - John D. Backes; Suzette Person; Neha Rungta; Oksana Tkachuk (SPIN, 2013)

Resolute: an assurance case language for architecture models. - Andrew Gacek; John Backes; Darren D. Cofer; Konrad Slind; Mike Whalen (HILT, 2014)

Requirements Analysis of a Quad-Redundant Flight Control System. - John Backes; Darren D. Cofer; Steven P. Miller; Michael W. Whalen (NFM, 2015)

Towards Realizability Checking of Contracts Using Theories. - Andrew Gacek; Andreas Katis; Michael W. Whalen; John Backes; Darren D. Cofer (NFM, 2015)

On Implementing Real-Time Specification Patterns Using Observers. - John D. Backes; Michael W. Whalen; Andrew Gacek; John Komp (NFM, 2016)

From Design Contracts to Component Requirements Verification. - Jing Liu; John D. Backes; Darren D. Cofer; Andrew Gacek (NFM, 2016)

Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability. - Andreas Katis; Grigory Fedyukovich; Andrew Gacek; John D. Backes; Arie Gurfinkel; Michael W. Whalen (CoRR, 2016)

The JKind Model Checker. - Andrew Gacek; John Backes; Mike Whalen; Lucas G. Wagner; Elaheh Ghassabani (CAV (2), 2018)

Semantic-based Automated Reasoning for AWS Access Policies using SMT. - John Backes; Pauline Bolignano; Byron Cook; Catherine Dodge; Andrew Gacek; Kasper Søe Luckow; Neha Rungta; Oksana Tkachuk; Carsten Varming (FMCAD, 2018)

Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. - Andreas Katis; Grigory Fedyukovich; Huajun Guo; Andrew Gacek; John Backes; Arie Gurfinkel; Michael W. Whalen (TACAS (2), 2018)

A Formal Approach to Constructing Secure Air Vehicle Software. - Darren D. Cofer; Andrew Gacek; John Backes; Michael W. Whalen; Lee Pike; Adam Foltzer; Michal Podhradsky; Gerwin Klein; Ihor Kuz; June Andronick; Gernot Heiser; Douglas Stuart (Computer, 2018)

Reachability Analysis for AWS-Based Networks. - John Backes; Sam Bayless; Byron Cook; Catherine Dodge; Andrew Gacek; Alan J. Hu; Temesghen Kahsai; Bill Kocik; Evgenii Kotelnikov; Jure Kukovec; Sean McLaughlin; Jason Reed 004; et al. (CAV (2), 2019)

One-Click Formal Methods. - John Backes; Pauline Bolignano; Byron Cook; Andrew Gacek; Kasper Søe Luckow; Neha Rungta; Martin Schäf; Cole Schlesinger; Rima Tanash; Carsten Varming; Michael W. Whalen (IEEE Softw., 2019)

Stratified Abstraction of Access Control Policies. - John Backes; Ulises Berrueco; Tyler Bray; Daniel Brim; Byron Cook; Andrew Gacek; Ranjit Jhala; Kasper Søe Luckow; Sean McLaughlin; Madhav Menon; Daniel Peebles; Ujjwal Pugalia; et al. (CAV (1), 2020)

Debugging Network Reachability with Blocked Paths. - Sam Bayless; John D. Backes; Dan DaCosta; Benjamin F. Jones 002; Nate Launchbury; Patrick Trentin; Kelsey Jewell; Sagar Joshi; Michael Q. Zeng; Nandita Mathews (CAV (2), 2021)

DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories. - Nick Feng; Alan J. Hu; Sam Bayless; Syed M. Iqbal; Patrick Trentin; Mike Whalen; Lee Pike; John Backes (TACAS (1), 2024)