About
I am a researcher working in Formal Methods and Programming Languages, using rigorous mathematical techniques to prove the correctness of computer programs. My broader background includes areas such as AI and Machine Learning, Computer Vision, Gesture Recognition, and Computer Security. I also bring over twenty years of industry experience across technical and business domains.
My recent research posts include postdoctoral scholar at Tufts University and Senior Research Associate at the University of Cambridge. I hold a Ph.D. in Electrical and Computer Engineering from Carnegie Mellon University and an M.S. in Computer Science from Colorado State University.
Publications
Peer-reviewed conferences and journals
- A CHERI C Memory Model for Verified Temporal Safety. CPP 2025.
- Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance. ASPLOS 2024.
- Modular, Compositional, and Executable Formal Semantics for LLVM IR. ICFP 2021.
- Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX. VSTTE 2020.
- Where's the Rock: Using Convolutional Neural Networks to Improve Land Cover Classification. Remote Sensing 2019.
- Passive User Identification Using Sequential Analysis of Proximity Information in Touchscreen Usage Patterns. ICMU 2015.
- Barometric and GPS Altitude Sensor Fusion. ICASSP 2014.
- 3D Finger Posture Detection and Gesture Recognition on Touch Surfaces. ICARCV 2012.
- HAMAKE: A Dataflow Approach to Data Processing in Hadoop. CLOSER 2012.
Workshops
- Research Report: Formally-Verified ASN.1 Protocol C-language Stack. LangSec 2020 (IEEE S&P Workshops).
- Reification of shallow-embedded DSLs in Coq with automated verification. CoqPL 2019.
- HELIX: A Case Study of a Formal Verification of High Performance Program Generation. FHPC 2018.
- Formal Verification of HCOL Rewriting. FMCAD 2015, Graduate Student Forum.
Preprints and technical reports
- HELIX: Verified Compilation of Cyber-Physical Control Systems to LLVM IR. Submitted to JFP, 2025. [HAL] [arXiv]
- Bridging Automated and Foundational Verification: Towards Translation Validation for CN Separation Logic Proofs. Working paper, 2025. [HAL]
- CHERI C semantics as an extension of the ISO C17 standard. Technical report, 2023. [UCAM-CL-TR-988]
- RSS XML Schema Grammar Induction. Technical report, 2014.
- Home Temperature Sensor Network. Technical report, 2013.
- Constructing an orthonormal set of eigenvectors for DFT matrix using Gramians and determinants. Preprint, 2012. [arXiv]
- Applying static code analysis to firewall policies for the purpose of anomaly detection. M.S. thesis, Colorado State University, 2009. [arXiv]
- Firewall Policy Modeling, Analysis and Simulation: a Survey. Preprint, 2008.
- Platform-Independent Firewall Policy Representation. Preprint, 2007. [arXiv]
- AccelKey Selection Method for Mobile Devices. Whitepaper, 2007. [arXiv]
- Enhanced "enclosures" support in RSS and ATOM Syndication. Specification proposal, 2004.
- Managing XML Documents Versions and Upgrades with XSLT. Technical report, 2001.
Articles
- Development of simple motion detection algorithm using Mathematica. FPROG.RU, 2011.
- Distributed builds with Rendezvous and DistCC. Dr. Dobb's Journal, 2004.
See my publications on DBLP and Google Scholar. For patents, see my patent list.
Personal
I was born in Ukraine 🇺🇦 and moved to the US in 1995. I have lived and worked in Silicon Valley since. Outside work, I enjoy literature, travelling, photography, and motorcycling.
Contact
I keep my business contacts organized via LinkedIn. I use Mastodon and my blog to write about technical matters.
- lord@crocodile.org
- Signal
- periplum.42
- vzaliva
- Mastodon
- @vzaliva@mastodon.acm.org
- GitHub
- @vzaliva
- Blog
- λ-Files