Correct and Complete Symbolic Execution for Free

{\AA}smund Aqissiaq Arild Kl{\o}vstad; Alexandra Silva; Einar Broch Johnsen; Erik Voogd; Jurriaan Rot

arxiv: 2606.21698 · v1 · pith:DETI2MMLnew · submitted 2026-06-19 · 💻 cs.PL

Correct and Complete Symbolic Execution for Free

Erik Voogd , Einar Broch Johnsen , {\AA}smund Aqissiaq Arild Kl{\o}vstad , Jurriaan Rot , Alexandra Silva This is my paper

Pith reviewed 2026-06-26 12:33 UTC · model grok-4.3

classification 💻 cs.PL

keywords symbolic executionoperational semanticsSOS rulescorrectnesscompletenessalgebraic signatureprogramming language semantics

0 comments

The pith

Symbolic SOS rules generate concrete and symbolic semantics that are provably correct and complete.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents symbolic SOS as a rule format for writing operational semantics that simultaneously define both concrete program execution and symbolic execution. It proves that the symbolic semantics obtained this way match the concrete semantics in both directions: every symbolic run corresponds to a concrete one and every concrete run is captured by the symbolic one. The construction uses only the algebraic signature of the language, so the same rules work across different languages without separate symbolic definitions. A reader would care because this removes the usual gap between ad-hoc symbolic executors and the language's actual behavior.

Core claim

Symbolic SOS is a rule format that allows simultaneous specification of concrete and symbolic operational semantics. When symbolic semantics are generated from symbolic SOS, they are both correct and complete with respect to the corresponding concrete semantics. The approach relies only on an algebraic signature of the source language.

What carries the argument

Symbolic SOS rule format that extends standard SOS rules to handle symbolic variables and side conditions while preserving the concrete semantics.

If this is right

Symbolic execution tools can be derived automatically from a single semantics specification.
Correctness and completeness hold uniformly for all languages fitting the rule format.
No separate proof is needed for each language's symbolic semantics.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The method could reduce duplication in verification frameworks that currently maintain separate concrete and symbolic interpreters.
Languages with non-SOS features such as higher-order effects or concurrency primitives might need extensions to the rule format before the guarantees apply.

Load-bearing premise

Any programming language can be given a complete operational semantics as a finite set of SOS rules over an algebraic signature.

What would settle it

A language whose semantics require rules outside finite SOS over an algebraic signature, or a program where the generated symbolic execution produces a path with no concrete counterpart.

Figures

Figures reproduced from arXiv: 2606.21698 by {\AA}smund Aqissiaq Arild Kl{\o}vstad, Alexandra Silva, Einar Broch Johnsen, Erik Voogd, Jurriaan Rot.

**Figure 1.** Figure 1: A symbolic SOS specification for the While language, from which both symbolic and concrete semantics can be derived. Example 3 (Specification for While). A symbolic SOS specification for the language system for While (from Example 2) is shown in [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗

read the original abstract

Symbolic execution is a powerful technique for program analysis. However, the formal semantics underlying symbolic execution is often developed on an ad-hoc basis and decoupled from the concrete semantics of the programming language. To overcome this issue, we introduce symbolic SOS: a rule format that allows us to simultaneously specify concrete and symbolic operational semantics. We prove that symbolic semantics, when generated from symbolic SOS, is both correct and complete with respect to the corresponding concrete semantics. The approach relies only on an algebraic signature of the source language, and is thus language-independent.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a symbolic SOS rule format that derives both concrete and symbolic semantics from the same rules plus a generic correctness and completeness proof, which is new if the details hold.

read the letter

The main contribution is a rule format called symbolic SOS that lets you write a single set of rules over an algebraic signature and obtain both the concrete operational semantics and a corresponding symbolic one, together with a proof that the symbolic version is correct and complete with respect to the concrete one. This is presented as language-independent because the proof does not depend on language-specific details beyond the signature and the finite rule set.

What works is the direct link between the two semantics. Most symbolic execution work builds the symbolic rules separately and by hand, which can introduce gaps or unsoundness. Here the claim is that following the format guarantees the properties without extra ad-hoc steps. That is a practical step forward for anyone who already has a standard SOS definition and wants symbolic execution without starting over.

The soft spots are around the scope and the missing details. The result only applies to languages that can be given a complete finite SOS semantics over an algebraic signature; anything with features outside that format falls outside the guarantee. Without the full paper we cannot check how the rule format is defined, how side conditions are managed, or whether the proof handles non-determinism and variable binding cleanly. The abstract states the claim clearly, but the actual derivation steps remain unexamined, so the soundness score stays provisional.

This is for researchers working on operational semantics, program analysis, and formal methods who need systematic ways to build verified symbolic tools across languages. A reader already using SOS would get value from seeing whether their languages fit the format and how the generated symbolic rules look in examples.

It deserves a serious referee to inspect the proof and the rule format in detail. The central idea is grounded enough to warrant that time.

Referee Report

0 major / 2 minor

Summary. The paper introduces symbolic SOS, a rule format that allows simultaneous specification of concrete and symbolic operational semantics for a programming language given only its algebraic signature. It proves that the symbolic semantics generated from symbolic SOS rules is both correct and complete with respect to the corresponding concrete semantics, and claims the result is language-independent.

Significance. If the proof is valid, the work supplies a reusable, signature-based method for obtaining verified symbolic execution semantics directly from standard SOS rules. This addresses the common problem of ad-hoc symbolic semantics and could improve the reliability of symbolic execution tools across languages by construction.

minor comments (2)

The abstract and introduction should explicitly restate the scope condition (finite SOS rules over an algebraic signature) as a prerequisite rather than only as a strength, to make the applicability limits clear to readers.
Add a small worked example (e.g., a simple imperative language fragment) showing how a concrete SOS rule is turned into its symbolic counterpart; this would make the generation process and the correctness argument easier to follow.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our paper and the recommendation of minor revision. No major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper's central result is a direct proof that symbolic semantics generated from a finite set of symbolic SOS rules over an algebraic signature is correct and complete w.r.t. the corresponding concrete semantics. This relationship is established by construction from the shared rule format and signature, without fitted parameters, self-referential definitions, or load-bearing self-citations. The derivation is self-contained as a language-independent theorem under the stated assumptions on the operational semantics format.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The approach rests on the assumption that languages are given by algebraic signatures and SOS rules; no free parameters are introduced. The new entity is the symbolic SOS rule format itself.

axioms (2)

domain assumption Every language of interest admits a complete operational semantics expressed as a finite set of SOS rules over an algebraic signature.
The abstract states that the method relies only on an algebraic signature; this presupposes that the concrete semantics can be captured in that form.
standard math Standard properties of algebraic signatures and SOS rule formats hold (e.g., substitution, congruence).
These are background facts from universal algebra and structural operational semantics invoked to support the generic proof.

invented entities (1)

symbolic SOS rule format no independent evidence
purpose: A single syntactic format from which both concrete and symbolic operational semantics can be derived automatically.
The format is introduced by the paper as the central technical device enabling the correctness and completeness result.

pith-pipeline@v0.9.1-grok · 5628 in / 1542 out tokens · 19200 ms · 2026-06-26T12:33:31.590520+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

27 extracted references · 14 canonical work pages

[1]

(eds.): Deductive Software Verification - The KeY Book - From Theory to Prac- tice, Lecture Notes in Computer Science, vol

Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Prac- tice, Lecture Notes in Computer Science, vol. 10001. Springer (2016).https: //doi.org/10.1007/978-3-319-49812-6

work page doi:10.1007/978-3-319-49812-6 2016
[2]

In: Erwig, M., Paige, R.F., Wyk, E.V

Arusoaie, A., Lucanu, D., Rusu, V.: A generic framework for symbolic execu- tion. In: Erwig, M., Paige, R.F., Wyk, E.V. (eds.) Software Language Engineer- ing - 6th International Conference, SLE 2013, Indianapolis, IN, USA, October 26-28, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8225, pp. 281–

2013
[3]

Springer (2013).https://doi.org/10.1007/978-3-319-02654-1_16,https: //doi.org/10.1007/978-3-319-02654-1_16

work page doi:10.1007/978-3-319-02654-1_16 2013
[4]

ACM Computing Surveys (CSUR)51(3), 1–39 (2018)

Baldoni, R., Coppa, E., D’elia, D.C., Demetrescu, C., Finocchi, I.: A survey of sym- bolic execution techniques. ACM Computing Surveys (CSUR)51(3), 1–39 (2018)

2018
[5]

In: Yi, K

Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) Proc. Third Asian Symposium on Programming Languages and Systems (APLAS 2005). Lecture Notes in Computer Science, vol. 3780, pp. 52–68. Springer (2005),https://doi.org/10.1007/11575467_5 18 E. Voogd et al

work page doi:10.1007/11575467_5 2005
[6]

Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. J. ACM42(1), 232––268 (Jan 1995).https://doi.org/10.1145/200836.200876

work page doi:10.1145/200836.200876 1995
[7]

Bodin, M., Gardner, P., Jensen, T., Schmitt, A.: Skeletal semantics and their inter- pretations. Proc. ACM Program. Lang.3(POPL) (jan 2019).https://doi.org/ 10.1145/3290357

work page doi:10.1145/3290357 2019
[8]

In: Proceedings of the 2015 Conference on Certified Programs and Proofs

Bodin, M., Jensen, T., Schmitt, A.: Certified abstract interpretation with pretty- big-step semantics. In: Proceedings of the 2015 Conference on Certified Programs and Proofs. p. 29–40. CPP ’15, Association for Computing Machinery (2015). https://doi.org/10.1145/2676724.2693174

work page doi:10.1145/2676724.2693174 2015
[9]

In: ter Beek, M.H., McIver, A., Oliveira, J.N

de Boer, F.S., Bonsangue, M.: On the nature of symbolic execution. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Formal Methods – The Next 30 Years. pp. 64–80. Springer International Publishing, Cham (2019)

2019
[10]

Formal As- pects of Computing33(4), 617–636 (2021)

de Boer, F.S., Bonsangue, M.: Symbolic execution formally explained. Formal As- pects of Computing33(4), 617–636 (2021)

2021
[11]

In: Shooman, M.L., Yeh, R.T

Boyer, R.S., Elspas, B., Levitt, K.N.: SELECT - a formal system for testing and debugging programs by symbolic execution. In: Shooman, M.L., Yeh, R.T. (eds.) Proc. International Conference on Reliable Software 1975. pp. 234–245. ACM (1975).https://doi.org/10.1145/800027.808445

work page doi:10.1145/800027.808445 1975
[12]

In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

Fragoso Santos, J., Maksimović, P., Ayoun, S.É., Gardner, P.: Gillian, part i: A multi-language platform for symbolic execution. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 927–942 (2020)

2020
[13]

van Glabbeek, R.J.: The meaning of negative premises in transition system specifications II. J. Log. Algebraic Methods Program.60-61, 229–258 (2004). https://doi.org/10.1016/J.JLAP.2004.03.007,https://doi.org/10.1016/j. jlap.2004.03.007

work page doi:10.1016/j.jlap.2004.03.007 2004
[14]

Leibniz International Proceedings in Informatics (LIPIcs), vol

Goncharov, S., Milius, S., Schröder, L., Tsampas, S., Urbat, H.: Stateful Structural OperationalSemantics.In:Felty,A.P.(ed.)7thInternationalConferenceonFormal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 228, pp. 30:1–30:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl...

work page doi:10.4230/lipics.fscd.2022.30 2022
[15]

Groote, J.F.: Transition system specifications with negative premises. Theor. Comput. Sci.118(2), 263–299 (1993).https://doi.org/10.1016/0304-3975(93) 90111-6,https://doi.org/10.1016/0304-3975(93)90111-6

work page doi:10.1016/0304-3975(93 1993
[16]

ACM SIGPLAN Notices10(6), 143–155 (1975)

Katz, S., Manna, Z.: Towards automatic debugging of programs. ACM SIGPLAN Notices10(6), 143–155 (1975)

1975
[17]

Communications of the ACM 19(7), 385–394 (1976)

King, J.C.: Symbolic execution and program testing. Communications of the ACM 19(7), 385–394 (1976)

1976
[18]

Klin, B., Nachyla, B.: Some undecidable properties of SOS specifications. J. Log. Algebraic Methods Program.87, 94–109 (2017).https://doi.org/10.1016/J. JLAMP.2016.08.005,https://doi.org/10.1016/j.jlamp.2016.08.005

work page doi:10.1016/j 2017
[19]

Journal of Symbolic Computation80, 125–163 (2017)

Lucanu, D., Rusu, V., Arusoaie, A.: A generic framework for symbolic execution: A coinductive approach. Journal of Symbolic Computation80, 125–163 (2017)

2017
[20]

In: Silva, A., Leino, K.R.M

Maksimović, P., Ayoun, S.É., Santos, J.F., Gardner, P.: Gillian, part II: Real-world verification for JavaScript and C. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification. pp. 827–850. Springer (2021)

2021
[21]

Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebraic Methods Program.60-61, 17–139 (2004), originally a tech. report from Aarhus University, 1981. Correct and Complete Symbolic Execution for Free 19

2004
[22]

Porncharoenwase, S., Nelson, L., Wang, X., Torlak, E.: A formal foundation for symbolic evaluation with merging. Proc. ACM Program. Lang.6(POPL) (jan 2022).https://doi.org/10.1145/3498709

work page doi:10.1145/3498709 2022
[23]

In: Peled, D., Pretschner, A

Rosu,G.:K-asemanticframeworkforprogramminglanguagesandformalanalysis tools. In: Peled, D., Pretschner, A. (eds.) Dependable Software Systems Engineer- ing. NATO Science for Peace and Security, IOS Press (2017)

2017
[24]

In: Dowek, G

Stefanescu, A., Ciobâcă, Ş., Mereuta, R., Moore, B.M., Serbanuta, T., Rosu, G.: All-path reachability logic. In: Dowek, G. (ed.) Proc. Joint International Con- ference on Rewriting and Typed Lambda Calculi (RTA-TLCA 2014). Lecture Notes in Computer Science, vol. 8560, pp. 425–440. Springer (2014),https: //doi.org/10.1007/978-3-319-08918-8_29

work page doi:10.1007/978-3-319-08918-8_29 2014
[25]

Steinhöfel, D.: Abstract execution: automatically proving infinitely many pro- grams. Ph.D. thesis, Technische Universität Darmstadt (2020)

2020
[26]

In: Pro- ceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science

Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: Pro- ceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science. pp. 280–291 (1997).https://doi.org/10.1109/LICS.1997.614955

work page doi:10.1109/lics.1997.614955 1997
[27]

by induction

Voogd, E., Johnsen, E.B., Silva, A., Susag, Z.J., Wasowski, A.: Symbolic semantics for probabilistic programs. In: Proc. 20th Intl. Conf. on Quantitative Evaluation of SysTems (QEST 2023). Lecture Notes in Computer Science, vol. 14287, pp. 329–345. Springer (2023) A Proofs In the proofs of Lemmas 1 and 2, we will use some universal algebra. The family εof...

2023

[1] [1]

(eds.): Deductive Software Verification - The KeY Book - From Theory to Prac- tice, Lecture Notes in Computer Science, vol

Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Prac- tice, Lecture Notes in Computer Science, vol. 10001. Springer (2016).https: //doi.org/10.1007/978-3-319-49812-6

work page doi:10.1007/978-3-319-49812-6 2016

[2] [2]

In: Erwig, M., Paige, R.F., Wyk, E.V

Arusoaie, A., Lucanu, D., Rusu, V.: A generic framework for symbolic execu- tion. In: Erwig, M., Paige, R.F., Wyk, E.V. (eds.) Software Language Engineer- ing - 6th International Conference, SLE 2013, Indianapolis, IN, USA, October 26-28, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8225, pp. 281–

2013

[3] [3]

Springer (2013).https://doi.org/10.1007/978-3-319-02654-1_16,https: //doi.org/10.1007/978-3-319-02654-1_16

work page doi:10.1007/978-3-319-02654-1_16 2013

[4] [4]

ACM Computing Surveys (CSUR)51(3), 1–39 (2018)

Baldoni, R., Coppa, E., D’elia, D.C., Demetrescu, C., Finocchi, I.: A survey of sym- bolic execution techniques. ACM Computing Surveys (CSUR)51(3), 1–39 (2018)

2018

[5] [5]

In: Yi, K

Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) Proc. Third Asian Symposium on Programming Languages and Systems (APLAS 2005). Lecture Notes in Computer Science, vol. 3780, pp. 52–68. Springer (2005),https://doi.org/10.1007/11575467_5 18 E. Voogd et al

work page doi:10.1007/11575467_5 2005

[6] [6]

Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. J. ACM42(1), 232––268 (Jan 1995).https://doi.org/10.1145/200836.200876

work page doi:10.1145/200836.200876 1995

[7] [7]

Bodin, M., Gardner, P., Jensen, T., Schmitt, A.: Skeletal semantics and their inter- pretations. Proc. ACM Program. Lang.3(POPL) (jan 2019).https://doi.org/ 10.1145/3290357

work page doi:10.1145/3290357 2019

[8] [8]

In: Proceedings of the 2015 Conference on Certified Programs and Proofs

Bodin, M., Jensen, T., Schmitt, A.: Certified abstract interpretation with pretty- big-step semantics. In: Proceedings of the 2015 Conference on Certified Programs and Proofs. p. 29–40. CPP ’15, Association for Computing Machinery (2015). https://doi.org/10.1145/2676724.2693174

work page doi:10.1145/2676724.2693174 2015

[9] [9]

In: ter Beek, M.H., McIver, A., Oliveira, J.N

de Boer, F.S., Bonsangue, M.: On the nature of symbolic execution. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Formal Methods – The Next 30 Years. pp. 64–80. Springer International Publishing, Cham (2019)

2019

[10] [10]

Formal As- pects of Computing33(4), 617–636 (2021)

de Boer, F.S., Bonsangue, M.: Symbolic execution formally explained. Formal As- pects of Computing33(4), 617–636 (2021)

2021

[11] [11]

In: Shooman, M.L., Yeh, R.T

Boyer, R.S., Elspas, B., Levitt, K.N.: SELECT - a formal system for testing and debugging programs by symbolic execution. In: Shooman, M.L., Yeh, R.T. (eds.) Proc. International Conference on Reliable Software 1975. pp. 234–245. ACM (1975).https://doi.org/10.1145/800027.808445

work page doi:10.1145/800027.808445 1975

[12] [12]

In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

Fragoso Santos, J., Maksimović, P., Ayoun, S.É., Gardner, P.: Gillian, part i: A multi-language platform for symbolic execution. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 927–942 (2020)

2020

[13] [13]

van Glabbeek, R.J.: The meaning of negative premises in transition system specifications II. J. Log. Algebraic Methods Program.60-61, 229–258 (2004). https://doi.org/10.1016/J.JLAP.2004.03.007,https://doi.org/10.1016/j. jlap.2004.03.007

work page doi:10.1016/j.jlap.2004.03.007 2004

[14] [14]

Leibniz International Proceedings in Informatics (LIPIcs), vol

Goncharov, S., Milius, S., Schröder, L., Tsampas, S., Urbat, H.: Stateful Structural OperationalSemantics.In:Felty,A.P.(ed.)7thInternationalConferenceonFormal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 228, pp. 30:1–30:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl...

work page doi:10.4230/lipics.fscd.2022.30 2022

[15] [15]

Groote, J.F.: Transition system specifications with negative premises. Theor. Comput. Sci.118(2), 263–299 (1993).https://doi.org/10.1016/0304-3975(93) 90111-6,https://doi.org/10.1016/0304-3975(93)90111-6

work page doi:10.1016/0304-3975(93 1993

[16] [16]

ACM SIGPLAN Notices10(6), 143–155 (1975)

Katz, S., Manna, Z.: Towards automatic debugging of programs. ACM SIGPLAN Notices10(6), 143–155 (1975)

1975

[17] [17]

Communications of the ACM 19(7), 385–394 (1976)

King, J.C.: Symbolic execution and program testing. Communications of the ACM 19(7), 385–394 (1976)

1976

[18] [18]

Klin, B., Nachyla, B.: Some undecidable properties of SOS specifications. J. Log. Algebraic Methods Program.87, 94–109 (2017).https://doi.org/10.1016/J. JLAMP.2016.08.005,https://doi.org/10.1016/j.jlamp.2016.08.005

work page doi:10.1016/j 2017

[19] [19]

Journal of Symbolic Computation80, 125–163 (2017)

Lucanu, D., Rusu, V., Arusoaie, A.: A generic framework for symbolic execution: A coinductive approach. Journal of Symbolic Computation80, 125–163 (2017)

2017

[20] [20]

In: Silva, A., Leino, K.R.M

Maksimović, P., Ayoun, S.É., Santos, J.F., Gardner, P.: Gillian, part II: Real-world verification for JavaScript and C. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification. pp. 827–850. Springer (2021)

2021

[21] [21]

Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebraic Methods Program.60-61, 17–139 (2004), originally a tech. report from Aarhus University, 1981. Correct and Complete Symbolic Execution for Free 19

2004

[22] [22]

Porncharoenwase, S., Nelson, L., Wang, X., Torlak, E.: A formal foundation for symbolic evaluation with merging. Proc. ACM Program. Lang.6(POPL) (jan 2022).https://doi.org/10.1145/3498709

work page doi:10.1145/3498709 2022

[23] [23]

In: Peled, D., Pretschner, A

Rosu,G.:K-asemanticframeworkforprogramminglanguagesandformalanalysis tools. In: Peled, D., Pretschner, A. (eds.) Dependable Software Systems Engineer- ing. NATO Science for Peace and Security, IOS Press (2017)

2017

[24] [24]

In: Dowek, G

Stefanescu, A., Ciobâcă, Ş., Mereuta, R., Moore, B.M., Serbanuta, T., Rosu, G.: All-path reachability logic. In: Dowek, G. (ed.) Proc. Joint International Con- ference on Rewriting and Typed Lambda Calculi (RTA-TLCA 2014). Lecture Notes in Computer Science, vol. 8560, pp. 425–440. Springer (2014),https: //doi.org/10.1007/978-3-319-08918-8_29

work page doi:10.1007/978-3-319-08918-8_29 2014

[25] [25]

Steinhöfel, D.: Abstract execution: automatically proving infinitely many pro- grams. Ph.D. thesis, Technische Universität Darmstadt (2020)

2020

[26] [26]

In: Pro- ceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science

Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: Pro- ceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science. pp. 280–291 (1997).https://doi.org/10.1109/LICS.1997.614955

work page doi:10.1109/lics.1997.614955 1997

[27] [27]

by induction

Voogd, E., Johnsen, E.B., Silva, A., Susag, Z.J., Wasowski, A.: Symbolic semantics for probabilistic programs. In: Proc. 20th Intl. Conf. on Quantitative Evaluation of SysTems (QEST 2023). Lecture Notes in Computer Science, vol. 14287, pp. 329–345. Springer (2023) A Proofs In the proofs of Lemmas 1 and 2, we will use some universal algebra. The family εof...

2023