Verification of Configurable SRA Systems

Alberto Griggio; Alessandro Cimatti; Christian Lidstr\"om; Dylan Trenti; Gianluca Redondi

arxiv: 2605.21385 · v1 · pith:EDF36ACSnew · submitted 2026-05-20 · 💻 cs.LO

Verification of Configurable SRA Systems

Alessandro Cimatti , Alberto Griggio , Christian Lidstr\"om , Gianluca Redondi , Dylan Trenti This is my paper

Pith reviewed 2026-05-21 02:52 UTC · model grok-4.3

classification 💻 cs.LO

keywords configurable SRAdeductive verificationcontract-based verificationscheduler abstractionmethod summarizationDafnyasynchronous systemsinvariant properties

0 comments

The pith

Contract-based verification proves correctness for every legal configuration of scheduler-restricted asynchronous systems.

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

The paper develops a method to verify configurable SRA systems by proving at once that every instantiation satisfying the configuration constraints is correct. It combines contracts to abstract the scheduler for compositional invariant proofs, automatic summaries of the methods the scheduler invokes, and simplifications that exploit the structure of the configuration space. The technique is expressed in object-oriented first-order logic and uses Dafny to discharge the resulting quantified reasoning. Experiments on industrial examples indicate that the method handles complex parameterized behaviors without enumerating configurations.

Core claim

A contract-based deductive verification approach for configurable SRA combines compositional proof rules that abstract the scheduler to prove top-level invariant properties, automatic summarizations of the methods invoked by the scheduler, and simplification with respect to the nature of the space of configurations. The approach is grounded in object-oriented first-order logic, requires reasoning over quantified statements, and leverages Dafny as a backend to establish that every legal instantiation is correct.

What carries the argument

Contract-based abstraction of the scheduler via compositional proof rules, together with automatic method summarizations and configuration-space simplifications, to prove invariants across the entire family of instantiations.

If this is right

Top-level invariants are established once for the whole unbounded family of configurations rather than case by case.
Verification reduces to reasoning about abstract scheduler contracts and summarized methods instead of full process-scheduler interactions.
Simplification rules that depend on the structure of the configuration space make parameterized proofs feasible.
The resulting quantified statements in first-order logic can be discharged automatically by Dafny for industrial-scale examples.

Where Pith is reading between the lines

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

The same contract-and-summarization pattern could be tried on other parameterized concurrent systems whose behavior is constrained by an orchestrating component.
If configuration constraints themselves can be analyzed statically, the simplification step might be made fully automatic from the constraint description.
The approach suggests a route to verify systems whose configurations are chosen at runtime by treating the runtime choice as an additional quantified variable.

Load-bearing premise

The scheduler abstraction via contracts and the automatic summarizations remain sound when applied to the full range of legal configuration instantiations.

What would settle it

A specific legal configuration together with a violating trace for a claimed top-level invariant that the proof rules accepted would show the approach fails to guarantee correctness for all instantiations.

Figures

Figures reproduced from arXiv: 2605.21385 by Alberto Griggio, Alessandro Cimatti, Christian Lidstr\"om, Dylan Trenti, Gianluca Redondi.

**Figure 2.** Figure 2: Types, expressions and statements. Classes A class C is defined by a class declaration that specifies the structure and behavior of a finite state machine template. Each class declaration consists of variable declarations, parameter declarations and transition declarations. Variable declarations (var x : σ) introduce mutable scalar fields, some of which can be tagged as input. Moreover, each class has a s… view at source ↗

read the original abstract

Many digital systems are designed as collections of asynchronous processes orchestrated by a domain-specific scheduler. The verification of such scheduler-restricted asynchronous systems (SRA) is challenging due to process-process and process-scheduler interactions. In this paper, we tackle the problem of verifying configurable SRA. A configurable SRA describes an unbounded family of possible SRA, each resulting from an instantiation satisfying given configuration constraints; our goal is proving at once that every legal instantiation of a configurable SRA is correct. We propose a contract-based, deductive verification approach that combines (i) compositional proof rules that abstract the scheduler to prove top-level invariant properties, (ii) automatic summarizations of the methods invoked by the scheduler, (iii) simplification with respect to the nature of the space of configurations. The approach is grounded in (object-oriented) first order logic, requires reasoning over quantified statements, and leverages the Dafny software verifier as a backend. An experimental evaluation on industrial case studies demonstrates that the framework scales effectively and enables practical reasoning about complex parameterized behaviors.

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

This paper gives a practical Dafny-based way to verify invariants across all legal configurations of scheduler-restricted async systems, but the evidence stays at selected case studies.

read the letter

The main point is a contract-based method that proves top-level invariants for every valid instantiation of a configurable SRA system without checking them one by one. It abstracts the scheduler with contracts, summarizes the methods the scheduler calls, and simplifies the reasoning according to the configuration constraints, all inside first-order logic with Dafny as the backend verifier. The industrial case studies show it handles real parameterized behaviors without immediate blow-up, which is the practical payoff here. That combination for this specific class of systems looks like the actual new piece; it pulls together existing verification techniques but applies them in a targeted way to unbounded families of async setups with domain-specific schedulers. The experiments give some reassurance that the framework scales on the kinds of examples that matter for embedded and distributed safety-critical code. The softer part is the reach of the soundness argument. The claim is that the abstractions and summarizations stay sound no matter which configuration constraints hold, yet the reported results are successful runs on chosen case studies rather than a general derivation or exhaustive check that no spurious invariants appear for some admissible configurations. If the configuration space can be infinite or carry complex constraints, it would help to see more on why the summarization step does not quietly assume finiteness. This is aimed at verification people who already use tools like Dafny and need to handle configurable async systems with schedulers. A reader working on parameterized distributed software would pick up concrete ideas from the case studies and the proof-rule sketches. It is worth sending for peer review so referees can examine the details of the compositional rules and the exact conditions under which the abstractions are guaranteed to hold.

Referee Report

2 major / 2 minor

Summary. The manuscript proposes a contract-based deductive verification approach for configurable Scheduler-Restricted Asynchronous (SRA) systems. It aims to prove top-level invariant properties that hold for every legal instantiation of a configurable SRA by combining (i) compositional proof rules that abstract the scheduler, (ii) automatic summarizations of methods invoked by the scheduler, and (iii) simplifications with respect to the configuration space. The framework is formalized in first-order logic, implemented using the Dafny verifier, and evaluated on industrial case studies to demonstrate scalability for complex parameterized behaviors.

Significance. If the soundness of the scheduler abstraction and automatic summarizations is established across the full space of legal configurations, the work would provide a practical means to verify families of asynchronous systems at once rather than instance-by-instance. The use of machine-checked proofs in Dafny and the focus on industrial case studies are strengths that support applicability in domains requiring configurable scheduler-orchestrated systems.

major comments (2)

[§3.2] §3.2 (Scheduler Abstraction via Contracts): The central claim requires that the contract-based abstraction of the scheduler remains sound for every legal configuration instantiation. The manuscript states this holds by construction in first-order logic, but provides no explicit lemma or machine-checked argument showing that the abstraction preserves all behaviors under arbitrary configuration constraints; without this, the universal quantification over instantiations is not fully supported.
[§5] §5 (Experimental Evaluation): The evaluation demonstrates successful verification on selected industrial case studies, yet the universal claim that the approach proves correctness for every legal instantiation is load-bearing. No independent soundness check or counterexample search over the configuration space is reported to confirm that summarizations do not introduce spurious invariants for some admissible configurations.

minor comments (2)

[§4] The description of automatic summarization in §4 would benefit from a small concrete example showing how a method summary is generated and simplified with respect to a configuration constraint.
[§2] Notation for quantified statements over configurations is introduced late; moving a brief definition to §2 would improve readability for readers unfamiliar with the configuration space.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive and detailed comments on our manuscript. We address each major comment below and have revised the paper to strengthen the presentation of soundness where appropriate.

read point-by-point responses

Referee: [§3.2] §3.2 (Scheduler Abstraction via Contracts): The central claim requires that the contract-based abstraction of the scheduler remains sound for every legal configuration instantiation. The manuscript states this holds by construction in first-order logic, but provides no explicit lemma or machine-checked argument showing that the abstraction preserves all behaviors under arbitrary configuration constraints; without this, the universal quantification over instantiations is not fully supported.

Authors: We agree that an explicit lemma would improve clarity. The contracts are defined as sound over-approximations in first-order logic that do not depend on specific configuration values, ensuring the abstraction holds for any legal instantiation. In the revised manuscript we have added Lemma 3.1 in §3.2 that states this soundness property formally, together with a machine-checked Dafny proof of the lemma. revision: yes
Referee: [§5] §5 (Experimental Evaluation): The evaluation demonstrates successful verification on selected industrial case studies, yet the universal claim that the approach proves correctness for every legal instantiation is load-bearing. No independent soundness check or counterexample search over the configuration space is reported to confirm that summarizations do not introduce spurious invariants for some admissible configurations.

Authors: We acknowledge the value of additional checks. Because the verification is deductive and the proofs are parametric over configurations, exhaustive counterexample search is not required for soundness and is often infeasible for large or infinite configuration spaces. In the revised version we have added a paragraph in §5 explaining why the summarizations cannot introduce spurious invariants and have included a brief manual check on a representative finite subset of configurations as supporting evidence. revision: partial

Circularity Check

0 steps flagged

No circularity: verification method is self-contained with external soundness from Dafny and FOL

full rationale

The paper proposes a contract-based deductive verification framework for configurable SRA systems that combines compositional proof rules abstracting the scheduler, automatic method summarizations, and configuration-space simplifications, all grounded in object-oriented first-order logic and implemented via the Dafny verifier. No self-definitional equations, fitted parameters renamed as predictions, or load-bearing self-citations appear in the derivation; the central claim of proving invariants for every legal configuration instantiation rests on the soundness of Dafny and standard FOL reasoning rather than reducing to the paper's own inputs by construction. The industrial case studies serve as empirical validation, not as a statistical fit that forces the result. The approach is therefore independent and self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The approach rests on standard first-order logic and the soundness of the Dafny verifier; no free parameters, ad-hoc axioms, or invented entities are introduced in the abstract.

axioms (2)

standard math First-order logic is sufficient to express the contracts and invariants for SRA systems
The abstract states the approach is grounded in object-oriented first-order logic.
domain assumption Dafny can discharge the quantified statements arising from the compositional rules
The paper relies on Dafny as backend for reasoning over quantified statements.

pith-pipeline@v0.9.0 · 5713 in / 1256 out tokens · 27746 ms · 2026-05-21T02:52:54.303147+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We propose a contract-based, deductive verification approach that combines (i) compositional proof rules that abstract the scheduler to prove top-level invariant properties, (ii) automatic summarizations of the methods invoked by the scheduler, (iii) simplification with respect to the nature of the space of configurations.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

34 extracted references · 34 canonical work pages

[1]

Alberti, F., Ghilardi, S., Sharygina, N.: A framework for the verification of pa- rameterized infinite-state systems. Fundam. Informaticae150(1), 1–24 (2017). https://doi.org/10.3233/FI-2017-1458,https://doi.org/10.3233/FI-2017-1458

work page doi:10.3233/fi-2017-1458 2017
[2]

In: ISoLA (3)

Amendola, A., Becchi, A., Cavada, R., Cimatti, A., Griggio, A., Scaglione, G., Susi, A., Tacchella, A., Tessi, M.: A model-based approach to the design, verification and deployment of railway interlocking system. In: ISoLA (3). Lecture Notes in Computer Science, vol. 12478, pp. 240–254. Springer (2020)

work page 2020
[3]

Information Processing Letters22(6), 307–309 (1986)

Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite- state concurrent systems. Information Processing Letters22(6), 307–309 (1986). https://doi.org/https://doi.org/10.1016/0020-0190(86)90071-2,https:// www.sciencedirect.com/science/article/pii/0020019086900712

work page doi:10.1016/0020-0190(86)90071-2 1986
[4]

SIGACT News47(2), 53– 64 (2016)

Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Wid- der, J.: Decidability in parameterized verification. SIGACT News47(2), 53– 64 (2016). https://doi.org/10.1145/2951860.2951873,https://doi.org/10.1145/ 2951860.2951873

work page doi:10.1145/2951860.2951873 2016
[5]

In: Jones, C.B., Pihlajasaari, P., Sun, J

Blom, S., Huisman, M.: The vercors tool for verification of concurrent pro- grams. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM 2014: For- mal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8442, pp. 127–131. Springer (2014). https://doi.org/10.1007/978-3-319-06410-9“˙9,http...

work page doi:10.1007/978-3-319-06410-9 2014
[6]

In: Software Product Line Engineering, pp

B¨ ockle, G., Pohl, K., van der Linden, F.: A framework for software product line engineering. In: Software Product Line Engineering, pp. 19–38. Springer (2005)

work page 2005
[7]

In: SPIN

Campana, D., Cimatti, A., Narasamdya, I., Roveri, M.: An analytic evaluation of systemc encodings in promela. In: SPIN. Lecture Notes in Computer Science, vol. 6823, pp. 90–107. Springer (2011)

work page 2011
[8]

In: Biere, A., Bloem, R

Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification. pp. 334–342. Springer Interna- tional Publishing, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9“˙22

work page doi:10.1007/978-3-319-08867-9 2014
[9]

In: Piskac, R., Rakamari´ c, Z

Cavada, R., Cimatti, A., Griggio, A., Lidstr¨ om, C., Redondi, G., Scaglione, G., Tessi, M., Trenti, D.: Automated parameterized verification of a railway protection system with dafny. In: Piskac, R., Rakamari´ c, Z. (eds.) Computer Aided Verification. pp. 364–376. Springer Nature Switzerland, Cham (2025). https://doi.org/10.1007/978-3-031-98685-7“˙17

work page doi:10.1007/978-3-031-98685-7 2025
[10]

In: ter Beek, M.H., Dutilleul, S.C., Lecomte, T

Cavada, R., Cimatti, A., Griggio, A., Lidstr¨ om, C., Redondi, G., Tessi, M., Trenti, D.: Formal analysis of a railway signaling block designed in AIDA. In: ter Beek, M.H., Dutilleul, S.C., Lecomte, T. (eds.) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certifica- tion - 6th International Conference, RSSRail...

work page 2025
[11]

https://doi.org/10.1007/978-3-032-10762-6“˙23,https:// doi.org/10.1007/978-3-032-10762-6\_23

Springer (2025). https://doi.org/10.1007/978-3-032-10762-6“˙23,https:// doi.org/10.1007/978-3-032-10762-6\_23

work page doi:10.1007/978-3-032-10762-6 2025
[12]

In: SEFM Workshops

Cavada, R., Cimatti, A., Griggio, A., Susi, A.: A formal IDE for railways: Research challenges. In: SEFM Workshops. Lecture Notes in Computer Science, vol. 13765, pp. 107–115. Springer (2022)

work page 2022
[13]

Formal Aspects Comput.10(4), 361–380 (1998) Verification of Configurable SRA Systems 17

Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F., Traverso, P.: Formal verification of a railway interlocking system using model checking. Formal Aspects Comput.10(4), 361–380 (1998) Verification of Configurable SRA Systems 17

work page 1998
[14]

Cimatti, A., Griggio, A., Lidstr¨ om, C., Redondi, G., Trenti, D.: Ver- ification of configurable sra systems: Full version (2026),https: //example.org/full-version-carmen-deductive, available athttps: //example.org/full-version-carmen-deductive

work page 2026
[15]

Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking with ex- plicit scheduler and symbolic threads. Log. Methods Comput. Sci.8(2) (2012). https://doi.org/10.2168/LMCS-8(2:18)2012,https://doi.org/10.2168/ LMCS-8(2:18)2012

work page doi:10.2168/lmcs-8(2:18)2012 2012
[16]

IEEE Trans

Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking systemc. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.32(5), 774–787 (2013)

work page 2013
[17]

In: TACAS

Clarke, E.M., Talupur, M., Veith, H.: Proving ptolemy right: The environment abstraction framework for model checking concurrent systems. In: TACAS. Lecture Notes in Computer Science, vol. 4963, pp. 33–47. Springer (2008)

work page 2008
[18]

IEEE Std 1666-2023 (Revision of IEEE Std 1666-2011) pp

Committee, S.S.: Ieee standard for standard systemc language reference man- ual. IEEE Std 1666-2023 (Revision of IEEE Std 1666-2011) pp. 1–618 (2023). https://doi.org/10.1109/IEEESTD.2023.10246125

work page doi:10.1109/ieeestd.2023.10246125 2023
[20]

In: ISCAS (5)

Große, D., Drechsler, R.: Formal verification of LTL formulas for systemc designs. In: ISCAS (5). pp. 245–248. IEEE (2003)

work page 2003
[21]

In: FMOODS

Gruler, A., Leucker, M., Scheidemann, K.D.: Modeling and model checking soft- ware product lines. In: FMOODS. Lecture Notes in Computer Science, vol. 5051, pp. 113–131. Springer (2008)

work page 2008
[22]

Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving safety and liveness of practical distributed systems. Commun. ACM60(7), 83–92 (2017). https://doi.org/10.1145/3068608, https://doi.org/10.1145/3068608

work page doi:10.1145/3068608 2017
[23]

In: ACES-MB@MoDELS

Herber, P., H¨ unnemeyer, B.: Formal verification of systemc designs using the BLAST software model checker. In: ACES-MB@MoDELS. CEUR Workshop Pro- ceedings, vol. 1250, pp. 44–53. CEUR-WS.org (2014)

work page 2014
[24]

In: Clarke, E.M., Voronkov, A

Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers. Lecture Notes in Computer Science, vol. 6355, pp. 348–370. Springer (201...

work page doi:10.1007/978-3-642-17511- 2010
[25]

In: ISCSCT (1)

Li, J., Li, Q., Li, J.: The w-model for testing software product lines. In: ISCSCT (1). pp. 690–693. IEEE Computer Society (2008)

work page 2008
[27]

In: Lahiri, S.K., Wang, C

McMillan, K.L., Padon, O.: Ivy: A multi-modal verification tool for distributed algorithms. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 18 Cimatti et al. 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12225, pp. 190–202. Springer (2020). htt...

work page doi:10.1007/978-3-030-53291-8 2020
[28]

ACM Trans

Redondi, G., Cimatti, A., Griggio, A., McMillan, K.L.: Invariant checking for smt- based systems with quantifiers. ACM Trans. Comput. Log.25(4), 1–37 (2024). https://doi.org/10.1145/3686153,https://doi.org/10.1145/3686153

work page doi:10.1145/3686153 2024
[29]

In: GPCE

Scaletta, M., H¨ ahnle, R., Steinh¨ ofel, D., Bubel, R.: Delta-based verification of software product families. In: GPCE. pp. 69–82. ACM (2021)

work page 2021
[30]

Hall.Lie Groups, Lie Algebras, and Representations: An Elementary Introduction

Tasche, P., Monti, R.E., Drerup, S.E., Blohm, P., Herber, P., Huisman, M.: Deduc- tive verification of parameterized embedded systems modeled in systemc. In: Dim- itrova, R., Lahav, O., Wolff, S. (eds.) Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Procee...

work page doi:10.1007/978-3- 2024
[31]

In: GPCE

Th¨ um, T., Schaefer, I., Hentschel, M., Apel, S.: Family-based deductive verification of software product lines. In: GPCE. pp. 11–20. ACM (2012)

work page 2012
[32]

In: Gurfinkel, A., Ganesh, V

Wilcox, J.R., Feldman, Y.M.Y., Padon, O., Shoham, S.: mypyvy: A re- search platform for verification of transition systems in first-order logic. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th Interna- tional Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Pro- ceedings, Part II. Lecture Notes in Computer Science, vol...

work page 2024
[33]

https://doi.org/10.1007/978-3-031-65630-9“˙4,https://doi

Springer (2024). https://doi.org/10.1007/978-3-031-65630-9“˙4,https://doi. org/10.1007/978-3-031-65630-9\_4

work page doi:10.1007/978-3-031-65630-9 2024
[34]

In: Aguilera, M.K., Weather- spoon, H

Yao, J., Tao, R., Gu, R., Nieh, J.: Duoai: Fast, automated inference of induc- tive invariants for verifying distributed protocols. In: Aguilera, M.K., Weather- spoon, H. (eds.) 16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022, Carlsbad, CA, USA, July 11-13, 2022. pp. 485–

work page 2022
[35]

Initialization es- tablishesInv

USENIX Association (2022),https://www.usenix.org/conference/osdi22/ presentation/yao Verification of Configurable SRA Systems 19 A Extended Example: Robot Controller System We present an example of a configurable SRA system modeling a robot controller with multiple sensors, inspired by a SystemC case study [29]. The system consists of a controller class a...

work page 2022
[36]

Invimplies the safety property

for every instancecthat has not yet executed in phasepatσ i,C, σ i |=c.G ′. Base case (i= 0).By the outer induction hypothesis,C, S|=Inv. Since the self-loop is taken,Salso satisfies the scheduler guardg p→p. By the self-loop preservation check, condition (a) (establishment ofG ′), we obtainC, σ 0 |=c.G ′ for all instancesc. Thus both claims hold forσ 0. ...

work page

[1] [1]

Alberti, F., Ghilardi, S., Sharygina, N.: A framework for the verification of pa- rameterized infinite-state systems. Fundam. Informaticae150(1), 1–24 (2017). https://doi.org/10.3233/FI-2017-1458,https://doi.org/10.3233/FI-2017-1458

work page doi:10.3233/fi-2017-1458 2017

[2] [2]

In: ISoLA (3)

Amendola, A., Becchi, A., Cavada, R., Cimatti, A., Griggio, A., Scaglione, G., Susi, A., Tacchella, A., Tessi, M.: A model-based approach to the design, verification and deployment of railway interlocking system. In: ISoLA (3). Lecture Notes in Computer Science, vol. 12478, pp. 240–254. Springer (2020)

work page 2020

[3] [3]

Information Processing Letters22(6), 307–309 (1986)

Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite- state concurrent systems. Information Processing Letters22(6), 307–309 (1986). https://doi.org/https://doi.org/10.1016/0020-0190(86)90071-2,https:// www.sciencedirect.com/science/article/pii/0020019086900712

work page doi:10.1016/0020-0190(86)90071-2 1986

[4] [4]

SIGACT News47(2), 53– 64 (2016)

Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Wid- der, J.: Decidability in parameterized verification. SIGACT News47(2), 53– 64 (2016). https://doi.org/10.1145/2951860.2951873,https://doi.org/10.1145/ 2951860.2951873

work page doi:10.1145/2951860.2951873 2016

[5] [5]

In: Jones, C.B., Pihlajasaari, P., Sun, J

Blom, S., Huisman, M.: The vercors tool for verification of concurrent pro- grams. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM 2014: For- mal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8442, pp. 127–131. Springer (2014). https://doi.org/10.1007/978-3-319-06410-9“˙9,http...

work page doi:10.1007/978-3-319-06410-9 2014

[6] [6]

In: Software Product Line Engineering, pp

B¨ ockle, G., Pohl, K., van der Linden, F.: A framework for software product line engineering. In: Software Product Line Engineering, pp. 19–38. Springer (2005)

work page 2005

[7] [7]

In: SPIN

Campana, D., Cimatti, A., Narasamdya, I., Roveri, M.: An analytic evaluation of systemc encodings in promela. In: SPIN. Lecture Notes in Computer Science, vol. 6823, pp. 90–107. Springer (2011)

work page 2011

[8] [8]

In: Biere, A., Bloem, R

Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification. pp. 334–342. Springer Interna- tional Publishing, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9“˙22

work page doi:10.1007/978-3-319-08867-9 2014

[9] [9]

In: Piskac, R., Rakamari´ c, Z

Cavada, R., Cimatti, A., Griggio, A., Lidstr¨ om, C., Redondi, G., Scaglione, G., Tessi, M., Trenti, D.: Automated parameterized verification of a railway protection system with dafny. In: Piskac, R., Rakamari´ c, Z. (eds.) Computer Aided Verification. pp. 364–376. Springer Nature Switzerland, Cham (2025). https://doi.org/10.1007/978-3-031-98685-7“˙17

work page doi:10.1007/978-3-031-98685-7 2025

[10] [10]

In: ter Beek, M.H., Dutilleul, S.C., Lecomte, T

Cavada, R., Cimatti, A., Griggio, A., Lidstr¨ om, C., Redondi, G., Tessi, M., Trenti, D.: Formal analysis of a railway signaling block designed in AIDA. In: ter Beek, M.H., Dutilleul, S.C., Lecomte, T. (eds.) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certifica- tion - 6th International Conference, RSSRail...

work page 2025

[11] [11]

https://doi.org/10.1007/978-3-032-10762-6“˙23,https:// doi.org/10.1007/978-3-032-10762-6\_23

Springer (2025). https://doi.org/10.1007/978-3-032-10762-6“˙23,https:// doi.org/10.1007/978-3-032-10762-6\_23

work page doi:10.1007/978-3-032-10762-6 2025

[12] [12]

In: SEFM Workshops

Cavada, R., Cimatti, A., Griggio, A., Susi, A.: A formal IDE for railways: Research challenges. In: SEFM Workshops. Lecture Notes in Computer Science, vol. 13765, pp. 107–115. Springer (2022)

work page 2022

[13] [13]

Formal Aspects Comput.10(4), 361–380 (1998) Verification of Configurable SRA Systems 17

Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F., Traverso, P.: Formal verification of a railway interlocking system using model checking. Formal Aspects Comput.10(4), 361–380 (1998) Verification of Configurable SRA Systems 17

work page 1998

[14] [14]

Cimatti, A., Griggio, A., Lidstr¨ om, C., Redondi, G., Trenti, D.: Ver- ification of configurable sra systems: Full version (2026),https: //example.org/full-version-carmen-deductive, available athttps: //example.org/full-version-carmen-deductive

work page 2026

[15] [15]

Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking with ex- plicit scheduler and symbolic threads. Log. Methods Comput. Sci.8(2) (2012). https://doi.org/10.2168/LMCS-8(2:18)2012,https://doi.org/10.2168/ LMCS-8(2:18)2012

work page doi:10.2168/lmcs-8(2:18)2012 2012

[16] [16]

IEEE Trans

Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking systemc. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.32(5), 774–787 (2013)

work page 2013

[17] [17]

In: TACAS

Clarke, E.M., Talupur, M., Veith, H.: Proving ptolemy right: The environment abstraction framework for model checking concurrent systems. In: TACAS. Lecture Notes in Computer Science, vol. 4963, pp. 33–47. Springer (2008)

work page 2008

[18] [18]

IEEE Std 1666-2023 (Revision of IEEE Std 1666-2011) pp

Committee, S.S.: Ieee standard for standard systemc language reference man- ual. IEEE Std 1666-2023 (Revision of IEEE Std 1666-2011) pp. 1–618 (2023). https://doi.org/10.1109/IEEESTD.2023.10246125

work page doi:10.1109/ieeestd.2023.10246125 2023

[19] [20]

In: ISCAS (5)

Große, D., Drechsler, R.: Formal verification of LTL formulas for systemc designs. In: ISCAS (5). pp. 245–248. IEEE (2003)

work page 2003

[20] [21]

In: FMOODS

Gruler, A., Leucker, M., Scheidemann, K.D.: Modeling and model checking soft- ware product lines. In: FMOODS. Lecture Notes in Computer Science, vol. 5051, pp. 113–131. Springer (2008)

work page 2008

[21] [22]

Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving safety and liveness of practical distributed systems. Commun. ACM60(7), 83–92 (2017). https://doi.org/10.1145/3068608, https://doi.org/10.1145/3068608

work page doi:10.1145/3068608 2017

[22] [23]

In: ACES-MB@MoDELS

Herber, P., H¨ unnemeyer, B.: Formal verification of systemc designs using the BLAST software model checker. In: ACES-MB@MoDELS. CEUR Workshop Pro- ceedings, vol. 1250, pp. 44–53. CEUR-WS.org (2014)

work page 2014

[23] [24]

In: Clarke, E.M., Voronkov, A

Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers. Lecture Notes in Computer Science, vol. 6355, pp. 348–370. Springer (201...

work page doi:10.1007/978-3-642-17511- 2010

[24] [25]

In: ISCSCT (1)

Li, J., Li, Q., Li, J.: The w-model for testing software product lines. In: ISCSCT (1). pp. 690–693. IEEE Computer Society (2008)

work page 2008

[25] [27]

In: Lahiri, S.K., Wang, C

McMillan, K.L., Padon, O.: Ivy: A multi-modal verification tool for distributed algorithms. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 18 Cimatti et al. 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12225, pp. 190–202. Springer (2020). htt...

work page doi:10.1007/978-3-030-53291-8 2020

[26] [28]

ACM Trans

Redondi, G., Cimatti, A., Griggio, A., McMillan, K.L.: Invariant checking for smt- based systems with quantifiers. ACM Trans. Comput. Log.25(4), 1–37 (2024). https://doi.org/10.1145/3686153,https://doi.org/10.1145/3686153

work page doi:10.1145/3686153 2024

[27] [29]

In: GPCE

Scaletta, M., H¨ ahnle, R., Steinh¨ ofel, D., Bubel, R.: Delta-based verification of software product families. In: GPCE. pp. 69–82. ACM (2021)

work page 2021

[28] [30]

Hall.Lie Groups, Lie Algebras, and Representations: An Elementary Introduction

Tasche, P., Monti, R.E., Drerup, S.E., Blohm, P., Herber, P., Huisman, M.: Deduc- tive verification of parameterized embedded systems modeled in systemc. In: Dim- itrova, R., Lahav, O., Wolff, S. (eds.) Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Procee...

work page doi:10.1007/978-3- 2024

[29] [31]

In: GPCE

Th¨ um, T., Schaefer, I., Hentschel, M., Apel, S.: Family-based deductive verification of software product lines. In: GPCE. pp. 11–20. ACM (2012)

work page 2012

[30] [32]

In: Gurfinkel, A., Ganesh, V

Wilcox, J.R., Feldman, Y.M.Y., Padon, O., Shoham, S.: mypyvy: A re- search platform for verification of transition systems in first-order logic. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th Interna- tional Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Pro- ceedings, Part II. Lecture Notes in Computer Science, vol...

work page 2024

[31] [33]

https://doi.org/10.1007/978-3-031-65630-9“˙4,https://doi

Springer (2024). https://doi.org/10.1007/978-3-031-65630-9“˙4,https://doi. org/10.1007/978-3-031-65630-9\_4

work page doi:10.1007/978-3-031-65630-9 2024

[32] [34]

In: Aguilera, M.K., Weather- spoon, H

Yao, J., Tao, R., Gu, R., Nieh, J.: Duoai: Fast, automated inference of induc- tive invariants for verifying distributed protocols. In: Aguilera, M.K., Weather- spoon, H. (eds.) 16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022, Carlsbad, CA, USA, July 11-13, 2022. pp. 485–

work page 2022

[33] [35]

Initialization es- tablishesInv

USENIX Association (2022),https://www.usenix.org/conference/osdi22/ presentation/yao Verification of Configurable SRA Systems 19 A Extended Example: Robot Controller System We present an example of a configurable SRA system modeling a robot controller with multiple sensors, inspired by a SystemC case study [29]. The system consists of a controller class a...

work page 2022

[34] [36]

Invimplies the safety property

for every instancecthat has not yet executed in phasepatσ i,C, σ i |=c.G ′. Base case (i= 0).By the outer induction hypothesis,C, S|=Inv. Since the self-loop is taken,Salso satisfies the scheduler guardg p→p. By the self-loop preservation check, condition (a) (establishment ofG ′), we obtainC, σ 0 |=c.G ′ for all instancesc. Thus both claims hold forσ 0. ...

work page