Meetings

Introduction The Formal Methods Group is a research subgroup at the Computing Science Department of Chalmers University of Technology. It was founded in 1997. The group is working with applying formal methods both in hardware and software. Hardware Description and Verification Hardware Verification The goal is to develop methods and tools for the design of correct circuits and systems. We have developed high performance SAT-solvers that are able to work incrementally, so that they are particualary good at solving a sequence of similar problems. Such problems arise for example when trying to verify properties of circuits over time. Here the solver MiniSat won all three industrial categories of the international SAT competition in 2005, showing that the technology is state of the art. There are however situations where propositional logic is simply not expressive enough. First order logic (FOL) offers higher expressiveness, while we can still retain a high degree of automation in proofs. We are developing a novel FOL theorem prover based on Stålmarck's mehtod of proof for propositional logic. We have also developed a tool called Paradox that finds finite-domain models of first order formulas. Here, again, we have showed immediate success in that Paradox won one of the classes in the international competition for FOL tools.             Members Wolfgang Ahrendt www e-mail Emil Axelsson www e-mail Magnus Björk www e-mail Koen Claessen www e-mail Niklas Eén www e-mail Tobias Gedell www e-mail Martin Giese www e-mail Reiner Hähnle www e-mail Wojciech Mostowski www e-mail Jan-Willem Roorda www e-mail Philipp Rümmer www e-mail Ingo Sander www e-mail Mary Sheeran www e-mail Hans Svensson www e-mail Niklas Sörensson www e-mail Angela Wallenburg www e-mail                   Hardware Description Our recent work focus on design methods where circuit performance is taken into account. As the size of components in integrated circuits continue to shrink, it is the routing of wires that account for most of the power consumption and signal dealy in the design. We therefore propose a design language, Wired, that aims to give the designer just the right amount of control over low level details. The new methods has been applied to the design of a multiplier that promises to be faster than existing designs. Our belief is that new design must both make use of ideas from computing science and take into account low level circuit details. This belif has led us to start a new collaboration with the VLSI Research Group (also at CSE). Together these two groups have a spread of competence that is not only necessary but unusual.

Formal Methods for Software