Formal study of functional orbits in finite domains

DOI10.1016/J.TCS.2014.10.041zbMATH Open1317.68208OpenAlexW2085828618MaRDI QIDQ483296FDOQ483296

Authors: Jean-François Dufourd 

Publication date: 16 December 2014

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2014.10.041

Recommendations

• Finite orbits for rational functions
• Finite polynomial orbits in finitely generated domains
• Integral orbits over function fields
• scientific article; zbMATH DE number 1522545
• Formal functions on prevalued domains
• Orbits of automorphisms of integral domains
• Orbits and continuity of certain class of functions
• Integrality estimates in orbits over function fields
• Coverage, invariability and orbits by structural functions
• Functions and functional on finite systems

zbMATH Keywords

program correctnessformal specificationCoq systemalgebraic data typecomputer-aided prooffunctional orbitslinked representationmemory shape analysis

Mathematics Subject Classification ID

Computer graphics; computational geometry (digital and algorithmic aspects) (68U05) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Cites Work

• N-DIMENSIONAL GENERALIZED COMBINATORIAL MAPS AND CELLULAR QUASI-MANIFOLDS
• Title not available (Why is that?)
• A Theorem on Boolean Matrices
• Title not available (Why is that?)
• Title not available (Why is that?)
• An axiomatic basis for computer programming
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Formal proof - the four color theorem
• Title not available (Why is that?)
• Iterated function systems and the global construction of fractals
• Rotors in Graph Theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• An efficient machine-independent procedure for garbage collection in various list structures
• Functional specification and prototyping with oriented combinatorial maps
• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• Formal study of plane Delaunay triangulation
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
• Proving pointer programs in higher-order logic
• Title not available (Why is that?)
• Design and formal proof of a new optimal image segmentation program with hypermaps
• Title not available (Why is that?)
• Generalised multi-pattern-based verification of programs with linear linked structures
• Hypermap specification and certified linked implementation using orbits
• Region-based shape analysis with tracked locations
• Shape Analysis for Composite Data Structures

Cited In (2)

• Simpler proofs with decentralized invariants
• Analysing the dynamics of digital chaotic maps via a new period search algorithm

Uses Software

• CGAL
• Coq
• CATIA V5
• CGoGN

This page was built for publication: Formal study of functional orbits in finite domains

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q483296)