Formally Verifying Optimizations with Block Simulations
L Gourdin, B Bonneau, S Boulmé, D Monniaux… - Proceedings of the …, 2023 - dl.acm.org
CompCert (ACM Software System Award 2021) is the first industrial-strength compiler with a
mechanically checked proof of correctness. Yet, CompCert remains a moderately optimizing …
mechanically checked proof of correctness. Yet, CompCert remains a moderately optimizing …
A survey of modern compiler fuzzing
H Ma - arXiv preprint arXiv:2306.06884, 2023 - arxiv.org
Most software that runs on computers undergoes processing by compilers. Since compilers
constitute the fundamental infrastructure of software development, their correctness is …
constitute the fundamental infrastructure of software development, their correctness is …
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier
Previous work on rewriting and reachability logic establishes a vision for a language-
agnostic program verifier, which takes three inputs: a program, its formal specification, and …
agnostic program verifier, which takes three inputs: a program, its formal specification, and …
Towards machine-readable semantic-based E-business contract representations using Network of Timed Automata (NTA)
P Qin, Q Hu, M Cui - Future Generation Computer Systems, 2024 - Elsevier
The smart contract is generally stored and executed by a computer program in the
blockchain platform. However, the representation of program code is unfriendly for non …
blockchain platform. However, the representation of program code is unfriendly for non …
TorchProbe: Fuzzing Dynamic Deep Learning Compilers
Static and dynamic computational graphs represent two distinct approaches to constructing
deep learning frameworks. The former prioritizes compiler-based optimizations, while the …
deep learning frameworks. The former prioritizes compiler-based optimizations, while the …
Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules
S Kommrusch, M Monperrus… - IEEE Transactions on …, 2023 - ieeexplore.ieee.org
We target the problem of automatically synthesizing proofs of semantic equivalence
between two programs made of sequences of statements. We represent programs using …
between two programs made of sequences of statements. We represent programs using …
Modeling Dynamic (De) Allocations of Local Memory for Translation Validation
A Rose, S Bansal - Proceedings of the ACM on Programming …, 2024 - dl.acm.org
End-to-End Translation Validation is the problem of verifying the executable code generated
by a compiler against the corresponding input source code for a single compilation. This …
by a compiler against the corresponding input source code for a single compilation. This …
Mechanizing matching logic in coq
P Bereczky, X Chen, D Horpácsi, L Peña… - arXiv preprint arXiv …, 2022 - arxiv.org
Matching logic is a formalism for specifying, and reasoning about, mathematical structures,
using patterns and pattern matching. Growing in popularity, it has been used to define many …
using patterns and pattern matching. Growing in popularity, it has been used to define many …
Self-Supervised Learning to Prove Equivalence Between Programs via Semantics-Preserving Rewrite Rules
S Kommrusch, M Monperrus - ArXivorg, 2021 - par.nsf.gov
We target the problem of automatically synthesizing proofs of semantic equivalence
between two programs made of sequences of statements. We represent programs using …
between two programs made of sequences of statements. We represent programs using …
WaveCert: Formal Compiler Validation for Asynchronous Dataflow Programs
Coarse-grained reconfigurable arrays (CGRAs), or dataflow architectures in general, have
gained attention in recent years due to their promising power efficiency compared to …
gained attention in recent years due to their promising power efficiency compared to …