Design and Verification of Algorithms

Consulting services by Dr. Wojciech Fraczak

I offer consultancy services in computer science and mathematics related to the software development: specification, modeling, design, implementation, and verification. Working for past 15 years on the frontier between Academia and Industry, I am well positioned to match practical algorithmic problems from the industry to the expertise (methods, tools, and research) coming from the academia.

My academic background covers formal languages and automata theory, models for concurrency, logic and theorem provers, graph algorithms, and programming and specification languages. I do not pretend to be experts in all aspects of computer science. In cases my competence is not enough for solving your problem, I can help you in finding the expertise in terms of research groups or individual researchers and connect them with you.

Why would you like to seek my services?

Complex systems and algorithms are difficult to elaborate and validate. Many formal approaches for design, development, and verification of computer systems exist, often backed by some software to guide and help the user. Unfortunately, most often the steep learning curve makes the formal method approaches rather difficult to use. Very different mathematical methods are used in different tools, even for addressing similar problems. There is little hope for finding "one tool to fit it all". Most often, many techniques have to be combined together in order to solve real practical problems.

My expertise can be of use for you if:

Specification and verification tools and methods I believe in.

There exist many tools built around numerous formal methods and no one can pretend to know them all. I keep learning about them constantly.

Standard formal methods

Z specification language, VDM (Vienna Development Method), Larch

Finite state methods

SPIN/Promella model checker, MONA project

Petri Nets and Timed Automata

PEP (Programming Environment based on Petri Nets), UPPAAL (timed automata)

Higher order logic and general theorem prover assistants

Coq, PVS