%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/
%% Created for Sebastiaan Joosten at 2024-03-18 13:31:45 -0500
%% Saved with string encoding Unicode (UTF-8)
@article{brogni2023translating,
author = {Brogni, Anthony and Joosten, Sebastiaan JC},
journal = {arXiv preprint arXiv:2308.02513},
title = {Translating First-Order Predicate Logic to Relation Algebra, Implemented using Z3},
year = {2023},
month = {7},
eprint={2308.02513},
local-url = {ARXIV2023Translating.pdf}}
@article{Joosten20,
abstract = {We formalize algebraic numbers in Isabelle/HOL. Our development serves as a verified implementation of algebraic operations on real and complex numbers. We moreover provide algorithms that can identify all the real or complex roots of rational polynomials, and two implementations to display algebraic numbers, an approximative version and an injective precise one. We obtain verified Haskell code for these operations via Isabelle's code generator. The development combines various existing formalizations such as matrices, Sturm's theorem, and polynomial factorization, and it includes new formalizations about bivariate polynomials, unique factorization domains, resultants and subresultants.},
author = {Joosten, Sebastiaan JC and Thiemann, Ren{\'e} and Yamada, Akihisa},
date-added = {2021-09-18 14:47:12 -0400},
date-modified = {2021-09-18 15:29:29 -0400},
journal = {Journal of automated reasoning},
local-url = {JAR2020AlgebraicNumbers.pdf},
month = {June},
number = {3},
pages = {363--389},
publisher = {Springer Netherlands},
title = {A verified implementation of algebraic numbers in Isabelle/HOL},
volume = {64},
year = {2020}}
@article{Divason20,
abstract = {We formally verify the Berlekamp--Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun's square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials. The algorithm first performs factorization in the prime field GF(𝑝) and then performs computations in the ring of integers modulo 𝑝𝑘, where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using locales and local type definitions. Through experiments we verify that our algorithm factors polynomials of degree up to 500 within seconds.},
author = {Divas{\'o}n, Jose and Joosten, Sebastiaan JC and Thiemann, Ren{\'e} and Yamada, Akihisa},
date-added = {2021-09-18 14:47:12 -0400},
date-modified = {2021-09-18 15:29:00 -0400},
journal = {Journal of automated reasoning},
local-url = {JAR2020BerlekampZassenhaus.pdf},
month = {June},
number = {4},
pages = {699--735},
publisher = {Springer Netherlands},
title = {A Verified Implementation of the Berlekamp--Zassenhaus Factorization Algorithm},
url = {https://zenodo.org/record/2539422},
volume = {64},
year = {2020},
bdsk-url-1 = {https://zenodo.org/record/2539422}}
@article{Thiemann20,
abstract = {The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has applications in number theory, computer algebra and cryptography. In this paper, we provide an implementation of the LLL algorithm. Both its soundness and its polynomial running-time have been verified using Isabelle/HOL. Our implementation is nearly as fast as an implementation in a commercial computer algebra system, and its efficiency can be further increased by connecting it with fast untrusted lattice reduction algorithms and certifying their output. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.},
author = {Thiemann, Ren{\'e} and Bottesch, Ralph and Divas{\'o}n, Jose and Haslbeck, Max W and Joosten, Sebastiaan JC and Yamada, Akihisa},
date-added = {2021-09-18 14:47:12 -0400},
date-modified = {2021-09-18 15:29:49 -0400},
journal = {Journal of Automated Reasoning},
local-url = {JAR20LLL.pdf},
month = {Jun},
number = {5},
pages = {827--856},
publisher = {Springer Netherlands},
title = {Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL},
volume = {64},
year = {2020}}
@inproceedings{Oortwijn20,
abstract = {Model checking algorithms are typically complex graph algorithms, whose correctness is crucial for the usability of a model checker. However, establishing the correctness of such algorithms can be challenging and is often done manually. Mechanising the verification process is crucially important, because model checking algorithms are often parallelised for efficiency reasons, which makes them even more error-prone. This paper shows how the VerCors concurrency verifier is used to mechanically verify the parallel nested depth-first search (NDFS) graph algorithm of Laarman et al. [25]. We also demonstrate how having a mechanised proof supports the easy verification of various optimisations of parallel NDFS. As far as we are aware, this is the first automated deductive verification of a multi-core model checking algorithm.},
author = {Oortwijn, Wytse and Huisman, Marieke and Joosten, Sebastiaan JC and van de Pol, Jaco},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems. 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25--30, 2020, Proceedings, Part I},
date-added = {2021-09-18 14:47:12 -0400},
date-modified = {2021-09-18 15:30:09 -0400},
month = {Apr},
organization = {Springer},
pages = {247--265},
title = {Automated verification of parallel nested DFS},
url = {https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/465629/4/Oortwijn2020_Chapter_AutomatedVerificationOfParalle.pdf},
volume = {12078},
year = {2020},
bdsk-url-1 = {https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/465629/4/Oortwijn2020_Chapter_AutomatedVerificationOfParalle.pdf}}
@inproceedings{Safari20,
abstract = {With the advent of dedicated hardware for multicore programming, parallel algorithms have become omnipresent. For example, various algorithms have been proposed for the parallel computation of a prefix sum in the literature. As the prefix sum is a basic building block for many other multicore algorithms, such as sorting, its correctness is of utmost importance. This means, the algorithm should be functionally correct, and the implementation should be thread and memory safe.
In this paper, we use deductive program verification based on permission-based separation logic, as supported by VerCors, to show correctness of the two most frequently used parallel in-place prefix sum algorithms for an arbitrary array size. Interestingly, the correctness proof for the second algorithm reuses the auxiliary lemmas that we needed to create the first proof. To the best of our knowledge, this paper is the first tool-supported verification of functional correctness of the two parallel in-place prefix sum algorithms which does not make any assumption about the size of the input array.},
author = {Safari, Mohsen and Oortwijn, Wytse and Joosten, Sebastiaan and Huisman, Marieke},
booktitle = {NASA Formal Methods Symposium},
date-added = {2021-09-18 14:47:12 -0400},
date-modified = {2021-09-18 15:28:09 -0400},
month = {Aug},
organization = {Springer, Cham},
pages = {170--186},
title = {Formal verification of parallel prefix sum},
url = {https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/465636/Safari2020_Chapter_FormalVerificationOfParallelPr.pdf?sequence=4},
year = {2020},
bdsk-url-1 = {https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/465636/Safari2020_Chapter_FormalVerificationOfParallelPr.pdf?sequence=4}}
@incollection{Mulder20,
abstract = {As program verification tools are becoming more powerful, and are used on larger programs, their performance also becomes more and more important. In this paper we investigate performance bottlenecks in the VerCors program verifier. Moreover, we also discuss two solutions to the identified performance bottlenecks: an improved encoding of arrays, as well as a technique to automatically generate trigger expressions to guide the underlying prover when reasoning about quantifiers. For both solutions we measure the effect on the performance. We see that the new encoding vastly reduces the verification time of certain programs, while other programs keep showing comparable times. This effect remains when moving to newer backends for VerCors.},
author = {Mulder, Henk and Huisman, Marieke and Joosten, Sebastiaan},
booktitle = {Deductive Software Verification: Future Perspectives},
date-added = {2021-09-18 14:47:12 -0400},
date-modified = {2021-09-18 15:27:36 -0400},
local-url = {DV2019VercorsPerformance.pdf},
month = {9},
pages = {65--82},
publisher = {Springer, Cham},
title = {Improving Performance of the VerCors Program Verifier},
year = {2020}}
@article{Joosten21a,
abstract = {This is a formalisation of the main result of Gale and Stewart from 1953, showing that closed finite games are determined. This property is now known as the Gale Stewart Theorem. While the original paper shows some additional theorems as well, we only formalize this main result, but do so in a somewhat general way. We formalize games of a fixed arbitrary length, including infinite length, using co-inductive lists, and show that defensive strategies exist unless the other player is winning. For closed games, defensive strategies are winning for the closed player, proving that such games are determined. For finite games, which are a special case in our formalisation, all games are closed.},
author = {Joosten, Sebastiaan JC},
date-added = {2021-09-18 14:47:12 -0400},
date-modified = {2021-09-18 15:26:48 -0400},
journal = {Arch. Formal Proofs},
month = {4},
title = {Gale-Stewart Games},
volume = {2021},
year = {2021}}
@article{Joosten21,
abstract = {This paper presents a set of online Discrete Mathematics exercises, and describe how
they were made. The motivation is threefold: First, to spread the word about an online
environment for doing Discrete Mathematics exercises, in the hope that others might
find it useful for their courses. Second, to describe experiential learning in a Functional
Programming class. Third, to invite feedback on Discrete Mathematics exercises and
suggestions for additional exercises.},
address = {Evansville, IN, USA},
author = {Joosten, Sebastiaan J. C.},
date-added = {2021-09-18 14:34:08 -0400},
date-modified = {2021-09-18 15:49:49 -0400},
issn = {1937-4771},
issue_date = {April 2021},
journal = {J. Comput. Sci. Coll.},
local-url = {CCSC21MathDrills.pdf},
month = {4},
number = {8},
numpages = {2},
pages = {107--108},
publisher = {Consortium for Computing Sciences in Colleges},
title = {Student-Made Online Discrete Math Drills: Lightning Talk},
volume = {36},
year = {2021}}
@article{Xu19,
abstract = {We formalise results from computability theory: recursive functions, undecidability of the halting problem, and the existence of a universal Turing machine. This formalisation is the AFP entry corresponding to the paper Mechanising Turing Machines and Computability Theory in Isabelle/HOL, ITP 2013.},
author = {Jian Xu and Xingyuan Zhang and Christian Urban and Sebastiaan Jozef Christiaan Joosten},
date-added = {2021-09-18 14:31:34 -0400},
date-modified = {2021-09-18 14:31:34 -0400},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = {2},
note = {Formal proof development},
title = {Universal Turing Machine},
url = {http://isa-afp.org/entries/Universal\_Turing\_Machine.html},
year = 2019,
bdsk-url-1 = {http://isa-afp.org/entries/Universal%5C_Turing%5C_Machine.html}}
@article{Joosten13a,
abstract = {Even though the ACL2 logic is first order, the ACL2 system offers several mechanisms providing users with some operations akin to higher order logic ones. In this paper, we propose a macro, named instance-of-defspec, to ease the reuse of abstract functions and facts proven about them. Defspec is an ACL2 book allowing users to define constrained functions and their associated properties. It contains macros facilitating the definition of such abstract specifications and instances thereof. Currently, lemmas and theorems derived from these abstract functions are not automatically instantiated. This is exactly the purpose of our new macro. instance-of-defspec will not only instantiate functions and theorems within a specification but also many more functions and theorems built on top of the specification. As a working example, we describe various fold functions over monoids, which we gradually built from arbitrary functions.},
author = {Joosten, Sebastiaan Jozef Christiaan and van Gastel, Bernard and Schmaltz, Julien},
day = {30},
journal = {arXiv preprint arXiv:1304.7875},
local-url = {ACL22013Macro.pdf},
month = {4},
note = {This paper was presented at the ACL2 Workshop 2013},
title = {A macro for reusing abstract functions and theorems},
year = {2013}}
@inproceedings{Verbeek13,
abstract = {Scalable formal verification constitutes an important challenge for the design of complicated asynchronous circuits. Deadlock freedom is a property that is desired but hard to verify. It is an emergent property that has to be verified monolithically. We propose to use Click, an existing library of asynchronous primitives, for verification. We present the automatic extraction of abstract SAT/SMT instances from circuits consisting of Click primitives. A theory is proven that opens the possibility of applying existing deadlock verification techniques for synchronous communication fabrics to asynchronous circuits.},
author = {Verbeek, Freek and Joosten, Sebastiaan Jozef Christiaan and Schmaltz, Julien},
booktitle = {Asynchronous Circuits and Systems (ASYNC), 2013 IEEE 19th International Symposium on},
doi = {10.1109/ASYNC.2013.21},
local-url = {ASYNC2013Click.pdf},
month = {May},
organization = {IEEE},
pages = {183--190},
title = {Formal deadlock verification for click circuits},
year = {2013},
bdsk-url-1 = {https://doi.org/10.1109/ASYNC.2013.21}}
@inproceedings{Joosten13,
abstract = {Communication fabrics constitute a key component of multicore processors and systems-on-chip. To ensure correctness of communication fabrics, formal methods such as model checking are essential. Due to the large number of buffers and the distributed character of control, applying these methods is challenging. Recent advancements in the verification of communication fabrics have demonstrated that the use of inductive invariants provides promising results towards scalable verification of Register Transfer Level (RTL) designs. In particular, these invariants are key in the verification of progress properties. Such invariants are difficult to infer. So far, they were either manually or automatically derived from a high-level description of the design. Important limitations of these approaches are the need for the high-level model and the necessary match between the model and the RTL design. We propose an algorithm to automatically derive these invariants directly from the RTL design. We consider communication fabrics to be a set of message storing elements (e.g, buffers) and some routing logic in-between. The only input required by our method is a definition of when messages enter or leave a buffer. We then exploit this well-defined buffer interface to automatically derive invariants about the number of packets stored in buffers. For several previously published examples, we automatically generate the exact same invariants that were either manually or automatically derived from a high-level model. Experimental results show that the time needed to generate invariants is a few seconds even for large examples.},
author = {Joosten, Sebastiaan Jozef Christiaan and Schmaltz, Julien},
booktitle = {Formal Methods and Models for Codesign (MEMOCODE), 2013 Eleventh IEEE/ACM International Conference on},
day = {18},
local-url = {MEMOCODE2013Generation.pdf},
month = {Oct},
organization = {IEEE},
pages = {57--64},
slides = {SlidesJoosten13.pdf},
title = {Generation of inductive invariants from register transfer level designs of communication fabrics},
year = {2013}}
@article{Joosten13b,
abstract = {The 3-partition problem admits a straightforward formulation as a 0-1 Integer Linear Program (ILP). We investigate problem instances for which the half-integer relaxation of the ILP is feasible, while the ILP is not. We prove that this only occurs on a set of at least 18 elements, and in case of 18 elements such an instance always contains an element of weight ≥ 10. These bounds are sharp: we give all 14 instances consisting of 18 elements all having weight ≤ 10. Our approach is based on analyzing an underlying graph structure.},
author = {Joosten, Sebastiaan Jozef Christiaan and Zantema, Hans},
day = {21},
local-url = {CTW2013Relaxation.pdf},
month = {May},
pdf = {CTW2013Relaxation},
publisher = {Enschede: University of Twente},
slides = {SlidesJoosten13b.pdf},
title = {Relaxation of 3-partition instances},
year = {2013}}
@mastersthesis{Joosten11,
author = {Joosten, Sebastiaan Jozef Christiaan},
date-modified = {2018-08-07 16:34:25 +0200},
day = {21},
local-url = {MSc2011Relaxations.pdf},
month = {Dec},
note = {[Slides in English](/publications/SlidesMScPresentation.pdf)},
school = {University of Twente},
slides = {SlidesMScPresentatie.pdf},
title = {Relaxations of the 3-partition problem},
year = {2011}}
@inproceedings{Michels11,
abstract = {Relation algebra can be used to specify information systems and business processes. It was used in practice in two large IT projects in the Dutch government. But which are the features that make relation algebra practical? This paper discusses these features and motivates them from an information system designer's point of view. The resulting language, Ampersand, is a syntactically sugared version of relation algebra. It is a typed language, which is supported by a compiler. The design approach, also called Ampersand, uses software tools that compile Ampersand scripts into functional specifications. This makes Ampersand interesting as an application of relation algebra in the industrial practice. The purpose of this paper is to define Ampersand and motivate its features from a practical perspective. This work is part of the research programme of the Information Systems & Business Processes (IS&BP) department of the Open University.},
author = {Michels, Gerard and Joosten, Sebastiaan Jozef Christiaan and van der Woude, Jaap and Joosten, Stef},
booktitle = {International Conference on Relational and Algebraic Methods in Computer Science},
doi = {10.1007/978-3-642-21070-9_21},
editor = {{Swart, de}, H.},
local-url = {RAMICS2011Ampersand.pdf},
month = {May},
organization = {Springer, Berlin, Heidelberg},
pages = {280--293},
title = {Ampersand: Applying Relation Algebra in Practice},
year = {2011},
bdsk-url-1 = {https://doi.org/10.1007/978-3-642-21070-9_21}}
@article{Joosten07,
author = {Joosten, Stef M M and Joosten, H. J M and Joosten, Sebastiaan Jozef Christiaan},
journal = {Informatie, juli/augustus, 42-50},
local-url = {Informatie2007Ampersand.pdf},
month = {Jul},
title = {Ampersand: foutvrije specificaties voor B\&I vraagstukken},
year = {2007}}
@inproceedings{Joosten14a,
abstract = {In the realm of multi-core processors and systems-on-chip, communication fabrics constitute a key element. A large number of queues and distributed control are two important aspects of this class of designs. These aspects make decomposition and abstraction techniques difficult to apply. For this class of designs, the application of formal methods is a real challenge. In particular, the verification of liveness properties is often intractable. Communication fabrics can be seen as a set of queues and flops interconnected by combinatorial logic. Based on this simple but powerful observation, we propose a novel method for liveness verification. Our method directly applies to Register Transfer Level designs. The essential aspects of our approach are (1) to abstract away from the details of queue implementations and (2) an efficient encoding of liveness properties in an SMT instance. Experimental results are promising. Designs with hundreds of queues can be analysed for liveness within minutes.},
author = {Joosten, Sebastiaan Jozef Christiaan and Schmaltz, Julien},
booktitle = {Design, Automation \& Test in Europe},
day = {24},
doi = {10.7873/DATE.2014.126},
local-url = {DATE2014Scalable.pdf},
month = {March},
organization = {European Design and Automation Association},
pages = {113},
title = {Scalable liveness verification for communication fabrics},
year = {2014},
bdsk-url-1 = {https://doi.org/10.7873/DATE.2014.126}}
@inproceedings{Joosten14,
abstract = {This paper reports our initial experiments with using external ATP on some corpora built with the ACL2 system. This is intended to provide the first estimate about the usefulness of such external reasoning and AI systems for solving ACL2 problems.},
author = {Joosten, Sebastiaan Jozef Christiaan and Kaliszyk, Cezary and Urban, Josef},
booktitle = {ACL2 Workhop},
doi = {10.4204/EPTCS.152.6},
local-url = {ACL22014Initial.pdf},
month = {Jul},
pages = {77--85},
slides = {SlidesJoosten14.pdf},
title = {Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems},
volume = {152},
year = {2014},
bdsk-url-1 = {https://doi.org/10.4204/EPTCS.152.6}}
@inproceedings{Joosten14b,
abstract = {In modern chip architectures, the increase in parallelisation brings about highly complex on-chip communication fabrics. We present WickedXmas, a tool that facilitates the design and formal verification of such interconnects. The tool is based on the language xMAS, which is a high level design language for communication fabrics, originally proposed by Intel. The use of xMAS ensures that many common modelling errors such as unintended loss of data or dangling wires are prevented by construction. Therefore, the major challenge in verifying xMAS models is establishing deadlock freedom. WickedXmas can automatically detect deadlocks or prove their absence. If a deadlock is found, it is presented to the user for further analysis. Experimental evaluation on a range of interconnects shows good performance and scalability of WickedXmas in contrast to verification from scratch, or using existing model checking techniques. Using WickedXmas, a user can draw a communication fabric and formally verify it automatically.},
author = {Joosten, Sebastiaan Jozef Christiaan and Verbeek, Freek and Schmaltz, Julien},
booktitle = {International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS)},
day = {20},
local-url = {DIFTS2014WickedXmas.pdf},
month = {Oct},
title = {WickedXmas: Designing and Verifying on-chip Communication Fabrics},
year = {2014}}
@inproceedings{Joosten15,
abstract = {Multi-core processors and Systems-on-Chips are composed of a large number of processing and memory elements interconnected by complex communication fabrics. These fabrics are large systems made of many queues and distributed control logic. Recent studies have demonstrated that high levels models of these networks are either tractable for verification or can provide key invariants to improve hardware model checkers. Formally verifying Register Transfer Level (RTL) designs of these networks is an important challenge, yet still open. This paper bridges the gap between high level models and RTL designs. We propose an algorithm that from a Verilog description automatically produces its corresponding micro-architectural model. We prove that the extracted model is transfer equivalent to the original RTL circuit. We illustrate our approach on a typical example of communication fabrics: a scoreboard with credit-flow control.},
author = {Joosten, Sebastiaan Jozef Christiaan and Schmaltz, Julien},
booktitle = {Design, Automation \& Test in Europe},
local-url = {DATE2015Automatic.pdf},
month = {Mar},
organization = {EDA Consortium},
pages = {1413--1418},
title = {Automatic extraction of micro-architectural models of communication fabrics from register transfer level designs},
year = {2015}}
@inproceedings{Joosten15a,
abstract = {In the process of incorporating subtyping in relation algebra, an algorithm was found to derive the subtyping relation from the program to be checked. By using domain analysis rather than type inference, this algorithm offers an attractive visualization of the type derivation process. This visualization can be used as a graphical proof that the type system has assigned types correctly. An implementation is linked to in this paper, written in Haskell. The algorithm has been tried and tested in Ampersand, a language that uses relation algebra for the purpose of designing information systems.},
author = {Joosten, Stef M M and Joosten, Sebastiaan Jozef Christiaan},
booktitle = {International Conference on Relational and Algebraic Methods in Computer Science},
doi = {10.1007/978-3-319-24704-5_14},
local-url = {RAMICS2015Type.pdf},
month = {Sep},
note = {[Get source code that accompanies the paper](http://cs.ru.nl/~B.Joosten/ampTypes/)},
organization = {Springer, Cham},
pages = {225--240},
slides = {SlidesJoosten15a.pdf},
title = {Type checking by domain analysis in {Ampersand}},
year = {2015},
bdsk-url-1 = {https://doi.org/10.1007/978-3-319-24704-5_14}}
@inproceedings{Wouda15,
abstract = {We propose an algorithm for reachability analysis in micro-architectural models of communication fabrics. The main idea of our solution is to group transfers in what we call transfer islands. In an island, all transfers fire at the same time. To justify our abstraction, we give semantics of the initial models using a process algebra. We then prove that a transfer occurs in the transfer islands model if and only if the same transfer occurs in the process algebra semantics. We encode the abstract micro-architectural model together with a given state reachability property in the input format of nuXmv. Reachability is solved either using BDDs or IC3. Combined with inductive invariant generation techniques, our approach shows promising results.},
author = {Wouda, Sanne and Joosten, Sebastiaan Jozef Christiaan and Schmaltz, Julien},
booktitle = {Formal Methods and Models for Codesign (MEMOCODE), 2015 ACM/IEEE International Conference on},
doi = {10.1109/MEMCOD.2015.7340487},
local-url = {MEMOCODE2015Process.pdf},
month = {Sep},
organization = {IEEE},
pages = {198--207},
title = {Process algebra semantics \& reachability analysis for micro-architectural models of communication fabrics},
year = {2015},
bdsk-url-1 = {https://doi.org/10.1109/MEMCOD.2015.7340487}}
@phdthesis{joosten2016verification,
abstract = {A communication fabric, or a Network on Chip (NoC), is a way to combine hardware components. For the final hardware to function correctly, it is critical that at least this NoC functions correctly. Some methods to prove the correctness of NoCs exist. An important property of correct NoCs, which turns out to be particularly difficult to prove, is that local deadlocks should not arise. We call NoCs live if they do not have such local deadlocks. Liveness proofs for networks that are large enough to be interesting in practice, used to exist only on an abstract level, or rely heavily on information from the abstract level.
To prove correctness of the concrete implementation of a NoC, we view the network as a set of queues an other state-holding elements, together with some combinational logic. This view lies very close to the actual hardware implementation. Queues and other state-holding elements are annotated through their interface. For this reason, we call this view on hardware the `interface level'.
The gate level implementation of a NoC design can be translated to combinational logic. At the gate level implementations, hardware designers make use of open wires and multi-directional gates. Where usual translations of gate level implementations are restricted to acyclic circuits with only binary gates, we show how to translate a richer class of gates to Boolean formulas. These Boolean formulas represent the gate level implementation of a NoC design.
In a proof about the correctness of a NoC, it can be important to know whether some queues can hold packets in a specific way. Linear one-step inductive invariants turn out to be a powerful tool to answer this question. Finding the right linear one-step inductive invariant used to require a high level description of the NoC. The essential property that is used describes when a packet of a certain type enters or leaves a queue: when a transfer occurs. By translating this property to a linear term, we can identify the linear invariants about the NoC. This property turns out to be available at the interface level. We describe how to translate this property to a linear term. As a consequence, we can automatically derive linear inductive invariants at the interface level.
To determine whether or not a NoC is live turns out to be very challenging. At the abstract level, there is a method that answer this question only partially: given a NoC, it can either prove that it is live, or it will present a situation which might be a reachable local deadlock. The latter case leaves the option open that the situation is not a reachable deadlock, in which case we still do not know whether or not the NoC is live. However, this methods has a good performance, and can determine liveness of NoCs of realistic sizes. We show that there is a similar algorithm at the interface level. Given a gate-level hardware description of a NoC, together with an interface specification of the queues, we formulate a Satisfiability Modulo Theory (SMT) problem that has an answer if the NoC has a reachable local deadlock. For many NoCs, the SMT problem turns out not to have an answer, which can be verified with standard SMT solvers. This proves that these NoCs are live, using only information that is available at the interface level.
We also reproduce an abstract-level description from the interface level. To do so, we give a procedure that constructs a tree of synchronising and arbitrating elements from the interface descriptions. Next, we orient the elements, deriving a graph in which all components are similar to the components in the xMAS language, a language for describing NoCs at an abstract level, proposed around 2010. For NoCs that were generated from xMAS, the resulting reproduced NoC is not necessarily equal to the original xMAS. Instead, we define a property called `transfer equivalence', and show that the resulting NoCs are transfer equivalent.
In addition to describing these novel techniques to analyse NoCs at the interface level, we have implemented the techniques as a proof of concept. Most of those implementations are now also available as part of a tool called Voi, which stands for `Verify on interfaces'. The tool Voi is implemented in Haskell, and we give some insight into its implementation. With this tool, we believe to have made a significant step towards the automated verification of gate-level descriptions of NoCs.},
author = {Joosten, Sebastiaan Jozef Christiaan},
date-modified = {2021-09-18 15:51:30 -0400},
day = {24},
local-url = {PhdThesisJoosten.pdf},
month = {Feb},
school = {Technische Universiteit Eindhoven},
title = {Verification of Interconnects},
url = {https://research.tue.nl/en/publications/verification-of-interconnects},
year = {2016},
bdsk-url-1 = {https://www.win.tue.nl/ipa/?event=verification-of-interconnects}}
@inproceedings{Divason16,
author = {Divas{\'o}n, Jose and Joosten, Sebastiaan Jozef Christiaan and Thiemann, Ren{\'e} and Yamada, Akihisa},
booktitle = {Isabelle Workshop},
local-url = {Isabelle2016Berlekamp.pdf},
month = {August},
title = {A Formalization of Berlekamp's Factorization Algorithm},
year = {2016}}
@article{Thiemann15,
abstract = {Based on existing libraries for matrices, factorization of rational polynomials, and Sturm's theorem, we formalized algebraic numbers in Isabelle/HOL. Our development serves as an implementation for real and complex numbers, and it admits to compute roots and completely factorize real and complex polynomials, provided that all coefficients are rational numbers. Moreover, we provide two implementations to display algebraic numbers, an injective and expensive one, or a faster but approximative version.
To this end, we mechanized several results on resultants, which also required us to prove that polynomials over a unique factorization domain form again a unique factorization domain.},
author = {Thiemann, Ren{\'e} and Yamada, Akihisa and Joosten, Sebastiaan Jozef Christiaan},
day = {22},
journal = {Archive of Formal Proofs},
month = {12},
title = {Algebraic Numbers in Isabelle/HOL},
url = {https://www.isa-afp.org/entries/Algebraic_Numbers.html},
volume = {2015},
year = {2015},
bdsk-url-1 = {https://www.isa-afp.org/entries/Algebraic_Numbers.html}}
@inproceedings{Joosten16,
author = {Joosten, Sebastiaan Jozef Christiaan and Thiemann, Ren{\'e} and Yamada, Akihisa},
booktitle = {15th International Workshop on Termination},
editor = {Middeldorp, Aart and Thiemann, Ren{\'e}},
local-url = {CeTA-WST16.pdf},
month = {Sep},
title = {CeTA--Certifying Termination and Complexity Proofs in 2016},
year = {2016}}
@inproceedings{Boerman18,
abstract = {To increase the impact and capabilities of formal verification, it should be possible to apply different verification techniques on the same specification. However, this can only be achieved if verification tools agree on the syntax and underlying semantics of the specification language and unfortunately, in practice, this is often not the case.In this paper, we concentrate on one particular example, namely Java programs annotated with JML, and we present a case study in understanding differences in the treatment of these specifications. Concretely, we take a collection of JML-annotated programs, that we tried to reverify using KeY and OpenJML. This effort led to a list of syntactical and semantical differences in the JML support between KeY and OpenJML. We discuss these differences, and then derive some general principles on how to improve interoperability between verification tools, based on the experiences from this case study.},
author = {Jan Boerman and Marieke Huisman and Joosten, Sebastiaan Jozef Christiaan},
booktitle = {iFM 2018, LNCS},
day = {5},
editor = {Furia, {Carlo A.} and Kirsten Winter},
language = {English},
local-url = {IFM2018KeyOpenJML.pdf},
month = {9},
pages = {1--17},
title = {Reasoning About JML: Differences Between KeY and OpenJML},
volume = {11023},
year = {2018}}
@conference{Joosten18a,
abstract = {Society nowadays relies heavily on software, which makes verifying the correctness of software crucially important. Various verification tools have been proposed for this purpose, each focusing on a limited set of tasks, as there are many different ways to build and reason about software. This paper discusses two case studies from the VerifyThis2018 verification competition, worked out using the VerCors verification toolset. Interestingly, these case studies are sequential, while VerCors specialises in reasoning about parallel and concurrent software. This paper elaborates on our experiences of using VerCors to verify sequential programs. The first case study involves specifying and verifying the behaviour of a gap buffer; a data-structure commonly used in text editors. The second case study involves verifying a combinatorial problem based on Project Euler problem #114. We find that VerCors is well capable of reasoning about sequential software, and that certain techniques to reason about concurrency can help to reason about sequential programs. However, the extra annotations required to reason about concurrency bring some specificational overhead.},
author = {Joosten, Sebastiaan Jozef Christiaan and Wytse Oortwijn and Mohsen Safari and Marieke Huisman},
day = {16},
language = {English},
month = {7},
note = {20th Workshop on Formal Techniques for Java-like Programs Formal techniques : FTfJP 2018 with ECOOP and ISSTA, FTfJP 2018 ; Conference date: 16-07-2018 Through 21-07-2018},
title = {An Exercise in Verifying Sequential Programs with VerCors},
url = {https://conf.researchr.org/track/FTfJP-2018/FTfJP-2018-papers},
year = {2018},
bdsk-url-1 = {https://conf.researchr.org/track/FTfJP-2018/FTfJP-2018-papers}}
@inbook{Divason18,
abstract = {The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It thereby approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has several applications in number theory, computer algebra and cryptography.In this paper, we develop the first mechanized soundness proof of the LLL algorithm using Isabelle/HOL. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.},
author = {Jose Divas{\'o}n and Sebastiaan Jozef Christiaan Joosten and Ren{\'e} Thiemann and Akihisa Yamada},
booktitle = {Interactive Theorem Proving},
day = {4},
doi = {10.1007/978-3-319-94821-8_10},
editor = {Jeremy Avigad and Assia Mahboubi},
isbn = {978-3-319-94820-1},
language = {English},
month = {7},
note = {Open Access},
pages = {160--177},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {A Formalization of the LLL Basis Reduction Algorithm},
year = {2018},
bdsk-url-1 = {https://doi.org/10.1007/978-3-319-94821-8_10}}
@inproceedings{Divason18d,
author = {Jose Divas{\'o}n and Joosten, {Sebastiaan Jozef Christiaan} and Ren{\'e} Thiemann and Akihisa Yamada},
booktitle = {16th International Workshop on Termination},
editor = {Salvador Lucas},
language = {English},
local-url = {WST2018PerronFrobenius.pdf},
month = {7},
pages = {30--34},
title = {A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving},
year = {2018}}
@article{Divason18c,
abstract = {Short vectors in lattices and factors of integer polynomials are related. Each factor of an integer polynomial belongs to a certain lattice. When factoring polynomials, the condition that we are looking for an irreducible polynomial means that we must look for a small element in a lattice, which can be done by a basis reduction algorithm. In this development we formalize this connection and thereby one main application of the LLL basis reduction algorithm: an algorithm to factor square-free integer polynomials which runs in polynomial time. The work is based on our previous Berlekamp--Zassenhaus development, where the exponential reconstruction phase has been replaced by the polynomial-time basis reduction algorithm. Thanks to this formalization we found a serious flaw in a textbook.},
author = {Jose Divas{\'o}n and Sebastiaan Jozef Christiaan Joosten and Ren{\'e} Thiemann and Akihisa Yamada},
day = {6},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
language = {English},
month = {2},
note = {Formal proof development},
publisher = {SourceForge},
title = {A verified factorization algorithm for integer polynomials with polynomial complexity},
url = {https://www.isa-afp.org/entries/LLL_Factorization.html},
year = {2018},
bdsk-url-1 = {https://www.isa-afp.org/entries/LLL_Factorization.html}}
@article{Joosten18,
abstract = {We give a procedure that can be used to automatically satisfy invariants of a certain shape. These invariants may be written with the operations intersection, composition and converse over binary relations, and equality over these operations. We call these invariants sentences that we interpret over graphs. For questions stated through sets of these sentences, this paper gives a semi-decision procedure we call graph saturation. It decides entailment over these sentences, inspired on graph rewriting. We prove correctness of the procedure. Moreover, we show the corresponding decision problem to be undecidable. This confirms a conjecture previously stated by the author.},
author = {Joosten, {Sebastiaan Jozef Christiaan}},
date-modified = {2018-11-23 10:32:45 +0100},
doi = {10.1016/j.jlamp.2018.06.005},
issn = {2352-2208},
journal = {Journal of Logical and Algebraic Methods in Programming},
keywords = {cs.LO, cs.DM, cs.PL},
language = {English},
local-url = {JLAMP2018Graph.pdf},
month = {11},
pages = {98--112},
publisher = {Elsevier BV},
title = {Finding models through graph saturation},
volume = {100},
year = {2018},
bdsk-url-1 = {https://doi.org/10.1016/j.jlamp.2018.06.005}}
@article{Divason18b,
abstract = {The Lenstra-Lenstra-Lov{\'a}sz basis reduction algorithm, also known as LLL algorithm, is an algorithm to find a basis with short, nearly orthogonal vectors of an integer lattice. Thereby, it can also be seen as an approximation to solve the shortest vector problem (SVP), which is an NP-hard problem, where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm also possesses many applications in diverse fields of computer science, from cryptanalysis to number theory, but it is specially well-known since it was used to implement the first polynomial-time algorithm to factor polynomials. In this work we present the first mechanized soundness proof of the LLL algorithm to compute short vectors in lattices. The formalization follows a textbook by von zur Gathen and Gerhard.},
author = {Jose Divas{\'o}n and Sebastiaan Jozef Christiaan Joosten and Ren{\'e} Thiemann and Akihisa Yamada},
day = {2},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
language = {English},
month = {2},
publisher = {SourceForge},
title = {A verified LLL algorithm},
url = {https://www.isa-afp.org/entries/LLL_Basis_Reduction.html},
volume = {2018},
year = {2018},
bdsk-url-1 = {https://www.isa-afp.org/entries/LLL_Basis_Reduction.html}}
@inproceedings{Divason17,
abstract = {We formalize the Berlekamp--Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun's square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials. The algorithm first performs a factorization in the prime field GF(p) and then performs computations in the ring of integers modulo pk, where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using Isabelle's recent addition of local type definitions. Through experiments we verify that our algorithm factors polynomials of degree 100 within seconds.},
address = {United States},
author = {Jose Divas{\'o}n and Sebastiaan Jozef Christiaan Joosten and Ren{\'e} Thiemann and Akihisa Yamada},
booktitle = {CPP 2017},
day = {16},
doi = {10.1145/3018610.3018617},
isbn = {978-1-4503-4705-1},
language = {English},
local-url = {CPP17_Berlekamp_Zassenhaus.pdf},
month = {Jan},
note = {[Formalisation is online](https://www.isa-afp.org/entries/Berlekamp_Zassenhaus.html)},
pages = {17--29},
publisher = {Association for Computing Machinery},
title = {A formalization of the Berlekamp-Zassenhaus factorization algorithm},
year = {2017},
bdsk-url-1 = {https://doi.org/10.1145/3018610.3018617}}
@inproceedings{Brockschmidt17,
abstract = {Modern program analyzers translate imperative programs to an intermediate formal language like integer transition systems (ITSs), and then analyze properties of ITSs. Because of the high complexity of the task, a number of incorrect proofs are revealed annually in the Software Verification Competitions.In this paper, we establish the trustworthiness of termination and safety proofs for ITSs. To this end we extend our Isabelle/HOL formalization IsaFoR by formalizing several verification techniques for ITSs, such as invariant checking, ranking functions, etc. Consequently the extracted certifier CeTA can now (in)validate safety and termination proofs for ITSs. We also adapted the program analyzers T2 and AProVE to produce machinereadable proof certificates, and as a result, most termination proofs generated by these tools on a standard benchmark set are now certified.},
author = {Marc Brockschmidt and Joosten, {Sebastiaan Jozef Christiaan} and Ren{\'e} Thiemann and Akihisa Yamada},
booktitle = {Automated Deduction - CADE 26 International Conference on Automated Deduction},
day = {11},
doi = {10.1007/978-3-319-63046-5_28},
editor = {{de Moura}, Leonardo},
isbn = {978-3-319-63045-8},
language = {English},
local-url = {CADE2017Certifying.pdf},
month = {Aug},
pages = {454--471},
publisher = {Springer},
series = {Lecture Notes in Artificial Intelligence},
title = {Certifying safety and termination proofs for integer transition systems},
year = {2017},
bdsk-url-1 = {https://doi.org/10.1007/978-3-319-63046-5_28}}
@inproceedings{Divason18a,
abstract = {Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of $A^n$ for a fixed non-negative rational matrix $A$. A direct solution for this task involves the computation of all eigenvalues of $A$, which often leads to expensive algebraic number computations.
In this work we formalize the Perron--Frobenius theorem. We utilize the theorem to avoid most of the algebraic numbers needed for certifying complexity analysis, so that our new algorithm only needs the rational arithmetic when certifying complexity proofs that existing tools can find. To cover the theorem in its full extent, we establish a connection between two different Isabelle/HOL libraries on matrices, enabling an easy exchange of theorems between both libraries. This connection crucially relies on the transfer mechanism in combination with local type definitions, being a non-trivial case study for these Isabelle tools.},
author = {Jose Divas{\'o}n and Sebastiaan Jozef Christiaan Joosten and Ondrej Kuncar and Ren{\'e} Thiemann and Akihisa Yamada},
booktitle = {Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs},
doi = {10.1145/3167103},
language = {English},
local-url = {CPPDivason18a.pdf},
month = {Jan},
pages = {2--13},
title = {Efficient certification of complexity proofs: formalizing the Perron--Frobenius theorem (invited talk paper)},
year = {2018},
bdsk-url-1 = {https://doi.org/10.1145/3167103}}
@inproceedings{Joosten17a,
abstract = {We introduce the tool Amperspiegel, which uses triple graphs for parsing, printing and manipulating data. We show how to conveniently encode parsers, graph manipulation-rules, and printers using several relations. As such, parsers, rules and printers are all encoded as graphs themselves. This allows us to parse, manipulate and print these parsers, rules and printers within the system. A parser for a context free grammar is graph-encoded with only four relations. The graph manipulation-rules turn out to be especially helpful when parsing. The printers strongly correspond to the parsers, being described using only five relations. The combination of parsers, rules and printers allows us to extract Ampersand source code from ArchiMate XML documents. Amperspiegel was originally developed to aid in the development of Ampersand.},
author = {Joosten, {Sebastiaan Jozef Christiaan}},
booktitle = {Relational and algebraic methods in computer science},
day = {16},
editor = {Peter H{\"o}fner and Damien Pous and Georg Struth},
isbn = {978-3-319-57417-2},
language = {English},
local-url = {RAMICS2017Parsing.pdf},
month = {May},
pages = {159--176},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
slides = {SlidesJoosten17a.pdf},
title = {Parsing and Printing of and with Triples},
year = {2017}}
@article{Joosten17,
abstract = {We formalize the theory of subresultants and the subresultant polynomial remainder sequence as described by Brown and Traub. As a result, we obtain efficient certified algorithms for computing the resultant and the greatest common divisor of polynomials.},
author = {Sebastiaan Jozef Christiaan Joosten and Ren{\'e} Thiemann and Akihisa Yamada},
day = {6},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
language = {English},
month = {4},
publisher = {SourceForge},
title = {Subresultants},
url = {https://www.isa-afp.org/entries/Subresultants.html},
year = {2017},
bdsk-url-1 = {https://www.isa-afp.org/entries/Subresultants.html}}