Software

Tree Logic Implementation: A Mu-Calculus Satisfiability Solver for Static Analysis

A system for checking XPath query containment, XPath query satisfiability under constraints (such as DTDs), XPath query equivalence, and many other related problems. The whole system is based on a new tree logic (see my publications) and mainly consists in:

a satisfiability solver for a μ-calculus with converse over finite trees;
compilers for translating XPath queries and regular tree grammars (including DTDs, XML Schemas, Relax NGs) into the logic;
a user-friendly predicate language that allow XML designers who are not familiar with the logic to directly formulate the static analysis problem of interest (query equivalence under constraints, forward compatibility fo schemas...) using native XML concepts (XPath, XML Schemas...).

The whole system is usable online as a web application: try it online! new! Its principle and architecture is illustrated below:

Old Commercial Software

A long time ago (in a galaxy far far away...), in my spare time (aka: my undergraduate studies) I have developed some software I found convenient. They finally happened to be marketed almost worldwide by a few (french, german, and canadian) software companies. I created WCK, one of the very first french web page editors in 1996. In 1999, I founded pierresoft.com. In 2001, I completed the design and development of Adesign: a graphic software for layered image authoring and retouching.