{'fraction_non_alphanumeric': 0.008771929824561403, 'fraction_numerical': 0.0, 'mean_word_length': 5.85, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Development of automatically verifiable systems using data representation synthesis

We present a technique for developing software that can be automatically formally verified for the absence of memory safety errors. Our technique makes use of Data Representation Synthesis to encapsulate all data structures inside within relational interfaces. We show that operations on relations can be precisely reasoned about using existing techniques for automatic precise reasoning on containers. In this work, we present a port of the Fiasco.OC microkernel to structures generated by Data Representation Synthesis that will be automatically verified by precise container reasoning techniques.