Travelled to:
1 × Australia
1 × Austria
1 × Germany
1 × Spain
2 × USA
Collaborated with:
∅ G.Nadathur M.W.Whalen E.Ghassabani D.Miller J.Backes L.G.Wagner Y.Wang K.Chaudhuri D.D.Cofer K.Slind D.Baelde A.Tiu M.P.E.Heimdahl M.Whalen S.Bayless B.Cook C.Dodge A.J.Hu T.Kahsai B.Kocik E.Kotelnikov J.Kukovec S.McLaughlin J.R.0004 N.Rungta J.Sizemore M.A.Stalzer P.Srinivasan P.Subotic C.Varming B.Whaley
Talks about:
model (3) specif (2) higher (2) relat (2) order (2) base (2) architectur (1) reachabl (1) properti (1) judgment (1)
Person: Andrew Gacek
DBLP: Gacek:Andrew
Contributed to:
Wrote 10 papers:
- HILT-2014-GacekBCSW #architecture #assurance #modelling #named
- Resolute: an assurance case language for architecture models (AG, JB, DDC, KS, MWW), pp. 19–28.
- PPDP-2013-WangCGN #higher-order #reasoning #relational #specification
- Reasoning about higher-order relational specifications (YW, KC, AG, GN), pp. 157–168.
- PPDP-2010-Gacek #higher-order #specification #syntax
- Relating nominal and higher-order abstract syntax specifications (AG), pp. 177–186.
- IJCAR-2008-Gacek #interactive #proving #theorem proving
- The Abella Interactive Theorem Prover (AG), pp. 154–161.
- LICS-2008-GacekMN #recursion
- Combining Generic Judgments with Recursive Definitions (AG, DM, GN), pp. 33–44.
- CADE-2007-BaeldeGMNT #model checking
- The Bedwyr System for Model Checking over Syntactic Expressions (DB, AG, DM, GN, AT), pp. 391–397.
- FSE-2016-GhassabaniGW #generative #induction #performance #safety
- Efficient generation of inductive validity cores for safety properties (EG, AG, MWW), pp. 314–325.
- ASE-2017-GhassabaniGWHW #metric #verification
- Proof-based coverage metrics for formal verification (EG, AG, MWW, MPEH, LGW), pp. 194–199.
- CAV-2018-GacekBWWG #model checking
- The JKind Model Checker (AG, JB, MW, LGW, EG), pp. 20–27.
- CAV-2019-BackesBCDGHKKKK #analysis #network #reachability
- Reachability Analysis for AWS-Based Networks (JB, SB, BC, CD, AG, AJH, TK, BK, EK, JK, SM, JR0, NR, JS, MAS, PS, PS, CV, BW), pp. 231–241.