Jix' Site

Projects

Varisat

Varisat is a CDCL based SAT solver written in rust. Given a boolean formula in conjunctive normal form, it either finds a variable assignment that makes the formula true or finds a proof that this is impossible.

[Read More]

Lower Size Bounds for Sorting Networks

I computed and formally verified the minimal number of required comparators in a sorting network with 11 and 12 inputs. This was an open problem. I’m currently writing a paper about this, and will add more information when this is completed. All the source code used, including a formal proof in Isabelle/HOL can be found at my sortnetopt GitHub project.

NECA - Not Even Coppersmith's Attack

This is a fast implementation of an attack by Rivest and Shamir adapted to work on 512-bit RSA keys affected by the ROCA vulnerability. I wrote a blog post describing the attack. The source code is available on GitHub.

Rust Libraries

Note that my SAT solver varisat, listed above, is also usable as a library.

ZwoHash

ZwoHash implements a very fast hash algorithm optimized for the use in hash tables. It has low per-hash overhead, which is important when hashing small keys. It is non-cryptographic and deterministic and as such not suited for inserting untrusted user-provided input into hash tables, unless other denial of service countermeasures are taken. As such it covers the same use cases as rustc’s FxHash.

See the GitHub project for more information.

vec_mut_scan

This library provides an iterator like interface over a vector which allows mutation and removal of items. Items are kept in order and every item is moved at most once, even when items are removed.

See the project on GitHub for more information.

partial_ref

The partial_ref library provides type checked partial references for rust. Type checked partial references are one solution to solve interprocedural borrowing conflicts. The partial_ref library makes it possible to safely pass references to partially borrowed structures between functions. Such code would normally be rejected by rust’s borrow checker.

[Read More]

Art Projects

Tanztatur

The “Tanztatur” is a meter-sized USB-keyboard you can walk and dance on. Presented at the 34c3, it was conceived by @TVLuke and me and built at the Nobreakspace. More pictures and details can be found on the project page (in German).

Demoscene Releases

I’ve been part of the demoscene since around 2007. Below is a selection of demoscene release I contributed to.

Overdrive 2

Overdrive is a Sega Mega Drive demo released at the Revision 2017 Demoparty where it won the 1st place in the alternative platform category. It also won the Meteoriks 2018 awards for outstanding technical achievement, best low-end production and a honorable mention for best soundtrack.

[Read More]

Overdrive

Overdrive is a Sega Mega Drive demo released at the Evoke 2013 Demoparty where it won the 1st place in the alternative platform category. I joined the project just before the deadline, to help completing it in time.

[Read More]

Runtime Verification

While working at the Institute for Software Engineering and Programming Languages of the University of Lübeck, I contributed to some projects in the area of runtime verfication.

Mufin–Runtime Monitoring with Union-Find Structures

Mufin is a tool that implements a runtime monitoring algorithm that can efficiently track properties that take hierarchical relationships of objects into account.

Using the union-find data structure, it can perform updates for multiple tracked objects simultaneously. It won the Java Track of the International Runtime Verification Competition 2016.

I contributed to the design of the final algorithm used and wrote an efficient implementation targeting the JVM. More information can be found on the official project page and in the corresponding paper.

Robotics