XML Static Analyzer User Manual
Pierre Geneves, Nabil Layaida
TL;DR
This manual explains how to use an XML static analyzer that verifies properties of XML documents by checking logical formulas derived from XPath, DTD, XML Schemas, and Relax NG, aiding in automated structural validation.
Contribution
It provides practical guidance for employing an XML reasoning solver that automates verification of structural and navigation properties in XML documents.
Findings
Supports verification of structural constraints and navigation properties.
Integrates XPath, DTD, XML Schemas, and Relax NG for property specification.
Enables automated, formal validation of XML document properties.
Abstract
This document describes how to use the XML static analyzer in practice. It provides informal documentation for using the XML reasoning solver implementation. The solver allows automated verification of properties that are expressed as logical formulas over trees. A logical formula may for instance express structural constraints or navigation properties (like e.g. path existence and node selection) in finite trees. Logical formulas can be expressed using the syntax of XPath expressions, DTD, XML Schemas, and Relax NG definitions.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Model-Driven Software Engineering Techniques · Logic, programming, and type systems