%0 Conference Proceedings
%T Translation Validation for Synchronous Data-Flow Specification in the SIGNAL Compiler
%+ Efficient STAtistical methods in SYstems of systems (ESTASYS)
%+ Tim, Events and Architectures (TEA)
%A Chan Ngo, Van
%A Talpin, Jean-Pierre
%A Gautier, Thierry
%Z Part 1: Ensuring Properties of Distributed Systems
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Grenoble, France
%Y Susanne Graf
%Y Mahesh Viswanathan
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-9039
%P 66-80
%8 2015-06-02
%D 2015
%R 10.1007/978-3-319-19195-9_5
%K Synchronous programs
%K Certified compiler
%K Translation validation
%K Formal verification
%K Graph transformation
%K Value-Graph
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X We present a method to construct a validator based on translation validation approach to prove the value-equivalence of variables in the compilation of the Signal compiler. The computation of output signals in a Signal program and their counterparts in the generated C code is represented by a Synchronous Data-flow Value-Graph (Sdvg). Our validator proves that every output signal and its counterpart variable have the same values by transforming the Sdvg graph.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01767328/document
%2 https://inria.hal.science/hal-01767328/file/978-3-319-19195-9_5_Chapter.pdf
%L hal-01767328
%U https://inria.hal.science/hal-01767328
%~ INSTITUT-TELECOM
%~ UNIV-RENNES1
%~ CNRS
%~ INRIA
%~ UNIV-UBS
%~ INSA-RENNES
%~ INRIA-RENNES
%~ IRISA
%~ IRISA_SET
%~ INRIA_TEST
%~ TESTALAIN1
%~ IFIP-LNCS
%~ IFIP
%~ CENTRALESUPELEC
%~ IRISA-D4
%~ INRIA2
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ UR1-HAL
%~ UR1-MATH-STIC
%~ IFIP-FORTE
%~ UR1-UFR-ISTIC
%~ TEST-UNIV-RENNES
%~ TEST-UR-CSS
%~ UNIV-RENNES
%~ INRIA-RENGRE
%~ IFIP-LNCS-9039
%~ INSTITUTS-TELECOM
%~ ANR
%~ UR1-MATH-NUM