Verified Generic Local Fixpoint Algorithms. - Aleksandr Karbyshev (AlgoSyn, 2010)

What Is a Pure Functional? - Martin Hofmann 001; Aleksandr Karbyshev; Helmut Seidl (ICALP (2), 2010)

Verifying a Local Generic Solver in Coq. - Martin Hofmann 001; Aleksandr Karbyshev; Helmut Seidl (SAS, 2010)

On Monadic Parametricity of Second-Order Functionals. - Andrej Bauer; Martin Hofmann 001; Aleksandr Karbyshev (FoSSaCS, 2013)

Monadic Parametricity of Second-Order Functionals. - Aleksandr Karbyshev (2013)

VeriCon: towards verifying controller programs in software-defined networks. - Thomas Ball 001; Nikolaj S. Bjørner; Aaron Gember; Shachar Itzhaky; Aleksandr Karbyshev; Mooly Sagiv; Michael Schapira; Asaf Valadarsky (PLDI, 2014)

Decentralizing SDN Policies. - Oded Padon; Neil Immerman; Aleksandr Karbyshev; Ori Lahav 001; Mooly Sagiv; Sharon Shoham (POPL, 2015)

Decidability of inferring inductive invariants. - Oded Padon; Neil Immerman; Sharon Shoham; Aleksandr Karbyshev; Mooly Sagiv (POPL, 2016)

Property-Directed Inference of Universal Invariants or Proving Their Absence. - Aleksandr Karbyshev; Nikolaj S. Bjørner; Shachar Itzhaky; Noam Rinetzky; Sharon Shoham (J. ACM, 2017)

Compositional Non-interference for Concurrent Programs via Separation and Framing. - Aleksandr Karbyshev; Kasper Svendsen; Aslan Askarov; Lars Birkedal (POST, 2018)

Computer-aided proofs for multiparty computation with active security. - Helene Haagh; Aleksandr Karbyshev; Sabine Oechsner; Bas Spitters; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2018)