2 March 2009Achim Brucker and Burkhart Wolff. Acta Informatica, 2009.
A new dichotomic algorithm for the uniform random generation of words in regular languages16 August 2012Johan Oudinet, Alain Denise, Marie-Claude Gaudel, Theoretical Computer Science (2012), DOI 10.1016/j.tcs.2012.07.025
Adaptation of Service Protocols Using Process Algebra and On-the-Fly Reduction Techniques8 August 2012An Extensible Encoding of Object-oriented Data Models in HOL with an Application to IMP++.20 October 2008In: Journal of Automated Reasoning (JAR), 2008.
Coverage-biased random explo-ration of large models and application to testing27 March 2011A. Denise, M.-C. Gaudel, S.-D. Gouraud, R. Lassaigne, J. Oudinet S. Peyronnet, STTT: Int. Jal on SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, DOI: 10.1007/s10009-011-0190-1
Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems22 March 2012HOL-Boogie - An Interactive Prover-Backend for the Verified C Compiler1 February 2010The paper describes a combined proof-environment for verification conditions generated for annotated C using automated and interactive proof techniques.
Model-Based Adaptation of Behavioral Mismatching Components1 September 2008Carlos Canal, Pascal Poizat and Gwen Salaün.
IEEE Transactions on Software Engineering, 34(4):546-563, 2008.
On Theorem Prover-based Testing10 January 2012HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. It allows for unit- sequence- and reactive sequence test in a uniform framework.
One step forward: Linking wireless self-organizing network validation techniques with formal testing approaches1 January 2011Proving Fairness and Implementation Correctness of a Microkernel Scheduler5 May 2009Matthias Daum , Jan Dörrenbächer and Burkhart Wolff.Journal of Automated Reasoning (JAR), 2009.
Uniform trace sampling in very large models6 November 2007A new algorithm makes it possible to draw traces uniformly at random in very large models of concurrent systems.
