About
I am a researcher with a focus on Formal Methods and Programming Languages. Over a career spanning twenty years in the industry, I've garnered a comprehensive understanding of both the technical and business facets of technology. While my core expertise lies in Formal Methods and Programming Languages, my academic interests are diverse and also include areas such as Machine Learning, Computer Vision, Gesture Recognition, and Computer Security.
Academic
I currently work on research in formal methods (using rigorous mathematical techniques to prove the correctness of computer programs) as a Senior Research Associate at the University of Cambridge. I have a Ph.D. from Carnegie Mellon University, M.S. in Computer Science, and B.S. in Electrical Engineering. (full CV)
Publications:
- Formal Mechanised Semantics of CHERI C: Capabilities, Provenance, and Undefined Behaviour. (preprint, ASPLOS 2024)
- CHERI C semantics as an extension of the ISO C17 standard (tech report, 2023)
- 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)
- Research Report: Formally-Verified ASN.1 Protocol C-language Stack (LangSec 2020)
- Where's the Rock: Using Convolutional Neural Networks to Improve Land Cover Classification (Remote Sensing 2019)
- 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)
- Passive User Identification Using Sequential Analysis of Proximity Information in Touchscreen Usage Patterns (ICMU 2015)
- Barometric and GPS Altitude Sensor Fusion (ICASSP 2014)
- Home Temperature Sensor Network (2013 project report)
- RSS XML Schema Grammar Induction (2014 project report)
- Constructing an orthonormal set of eigenvectors for DFT matrix using Gramians and determinants (2012)
- 3D Finger Posture Detection and Gesture Recognition on Touch Surfaces (ICARCV 2012)
- HAMAKE: A Dataflow Approach to Data Processing in Hadoop (CLOSER 2012)
- Developement of simple motion detection algorithm using Mathematica (FPROG.RU, 2011, russian)
- Applying static code analysis to firewall policies for the purpose of anomaly detection (2009)
- Firewall Policy Modeling, Analysis and Simulation: a Survey (2008)
- Platform-Independent Firewall Policy Representation (2007)
- Using UsernameToken Authentication with Blogger and MetaWebLog APIs (2007)
- Enhanced "enclosures" support in RSS and ATOM Syndication (2004)
- "AccelKey" input method whitepaper (2006)
- Distributed builds with Rendezvous and DistCC (Dr. Dobb's Journal, 2004)
- Managing XML Documents Versions and Upgrades with XSLT (2001)
- (my patents)
Business
Since 2004, I have been running a consulting business helping startups to build innovative software products. We have a team of about 100 highly skilled engineers who are able to tackle any technical challenge. To learn more, please visit Codeminders website.
Since 2016, Digamma.ai is the artificial intelligence and machine learning branch of Codeminders. We have over a decade of experience in developing tailored AI solutions — including complex machine learning, natural language processing, and computer vision technologies — for entrepreneurs, startups, and Fortune 500 companies.
Personal
Born in Ukraine, I moved to the US in 1995 and have been living and working in Silicon Valley ever since. I've been fortunate to find a job I love, and it feels less like work and more like passion. Outside of my professional endeavours, I enjoy literature, travelling, photography, and motorcycling.
Contacts
My contact information is below. I keep my business contacts organized via LinkedIn. I use Mastodon and my blog to write about technical matters.
- Email lord@crocodile.org
- Signalperiplum.42
- LinkedIn vzaliva
- Mastodon @vzaliva@mastodon.acm.org
- GitHub @vzaliva
- Technical Blog lambda-files.crocodile.org