Note: Below are abstracts for invited talks and abstracts for rump session talks.
| INVITED TALKS | |
| Jade Alglave (Arm, Inc. and University College London) |
Armed cats: formal concurrency modelling at Arm
In this talk I will give an overview of the work conducted by my team at Arm: we look after the memory model. In practice this means that we maintain and enhance a formal artefact called a cat file, which contains the requirements that the Arm architecture prescribes in terms of concurrency. We also maintain and enhance a set of companion tools (see diy.inria.fr and https://github.com/herd/herdtools7): the herd simulator, which determines whether a given concurrent behaviour (a litmus test) is allowed or not by the cat file, the diy test generator, which can generate vast systematic families of litmus tests automatically, and the litmus tool, which can run those tests on deployed hardware. I will give an overview of the various developments since I joined Arm in 2018, for example: mixed-size accesses and page-table related orderings. Please do see the following for further reading:
How to use the herd7 simulator: How to generate tests with the diy7 test generator (including a configuration file to feed to diy to generate interesting tests):
How to run tests on deployed hardware with the litmus7 tool: How we have extended our testing and modelling to page table related concerns: |
| Marijn Heule (Carnegie Mellon University) |
Effective Encodings for Computer-Aided Mathematics
Progress in satisfiability (SAT) solving has made it possible to determine the correctness of complex systems and answer long-standing open questions in mathematics. Recent successes in computer-aided mathematics were due to effective, but complex encodings into SAT. The SAT solving approach is automatic and can produce clever though potentially gigantic proofs. We can have confidence in the correctness of the answers because highly trustworthy systems can validate the underlying proofs regardless of their size. Yet to fully trust the results, we would need to verify the encodings as well. In this talk, we present two recent successes. The first is the resolution of Keller's conjecture, a long-standing open problem regarding tiling the n-dimensional space. In contrast to other successes using SAT, designing an effective encoding for this problem was far from trivial. The used encoding is many orders of magnitude smaller compared to straightforward encodings and it was crucial to finally solve this problem. The second success is a novel encoding of the Hamiltonian cycle problem into SAT, called the Chinese remainder encoding. We show that the encoding is more effective on hard Hamiltonian cycle problems compared to other proposed encodings. We finally discuss some challenges to verify these encodings. |
| RUMP SESSION TALKS | |
| Jagadish Bapanapally Ruben Gamboa |
Integration by Substitution in ACL2(r)
A theory of differentiation and integration, including several algebraic rules of differentiation and integration, have been previously formalized in ACL2(r). As an extension, we present a formalization of the method of Integration by Substitution, also known as u-substitution. This method is often used in calculus to find the integral of a function. Finding the integral of a function is sometimes complicated using the existing differentiation rules in ACL2(r), especially for functions with complicated antiderivates. But many such functions can be integrated more easily after a change of coordinates, so the u-substitution method is very useful. We show the formalization of u-substitution using the fundamental theorem of calculus and the chain rule which are already proved in ACL2(r) and demonstrate the application of u-substitution with two examples. |
| Ruben Gamboa | Accessing ACL2 Through Jupyter Notebooks
[Slides] |
| Jagadish Bapanapally Ruben Gamboa |
Towards Partial Differentiation in ACL2(r)
Currently, continuity in ACL2(r) is defined on a single variable and so the differentiation and integration can be applied to functions that have one variable. We want to add a second argument to the real continuous function that is constant while the function varies with the first argument. The constant can be a single value or a list of values, e.g., f(x, [y, z]). This allows us to do differentiation with respect to one variable while keeping the other constant. We are currently working to make this change to the ACL2(r) books. The change will result in some incompatibilities with prior work, and we will fix all the community books. Eventually, we will be able to do partial differentiation and integrate functions with two or more variables. |
| Shilpi Goel | Bigmem
[Slides] In this talk, I will present bigmem, a space-efficient implementation of a memory model of up to 2^64 bytes that offers near constant-time access and supports efficient reasoning. Bigmem uses nested and abstract stobjs to provide a simple, general, and reusable solution to the problem of modeling a large memory in ACL2. In the ACL2 Community books, it is used to specify the memory component of the state in the x86isa model. |