Posts

Automation instead of BibTeX reference sheets! I explain how to use online bibliographies, cite online resources, use BibTeX linters, and automatically reformat BibTeX files to obtain valid and complete bibliographies as well as tidy .bib files.

State merging is a standard technique for mitigating path explosion in symbolic execution. Nondeterministic value summaries are guarded sets of values with overlapping guards. Without those, we cannot perform fully precise state merging in all situations (do-while loops, unstructured code, nondeterministic programs). Reconstructing symbolic execution traces from states merged with nondeterministic value summaries requires some notion of time or origin.

My PhD thesis “Abstract Execution: Automatically Proving Infinitely Many Programs” has been published and is available for download (open access). The abstract and possible errata found after publication are listed on a separate page.

Presentation of a script for using Inkscape as an editor for animations in LaTeX presentations.