## Found 15,224 Documents (Results 1–100)

100
MathJax

### The refinement calculus of reactive systems. (English)Zbl 07538310

MSC:  68Q60 68V20
Full Text:

### Robust, expressive, and quantitative linear temporal logics: pick any two for free. (English)Zbl 07538307

MSC:  68Q60 03B44
Full Text:

Full Text:

### Model checking QCTL plus on quantum Markov chains. (English)Zbl 1483.68212

MSC:  68Q60 03B44 81P68
Full Text:

Full Text:

Full Text:

### Configurable verification of timed automata with discrete variables. (English)Zbl 1483.68208

MSC:  68Q60 68Q45
Full Text:

Full Text:

### Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL. (English)Zbl 07498610

MSC:  68Q60 68V15
Full Text:

### Model checking, synthesis, and learning. Essays dedicated to Bengt Jonsson on the occasion of his 60th birthday. (English)Zbl 07497120

Lecture Notes in Computer Science 13030. Cham: Springer (ISBN 978-3-030-91383-0/pbk; 978-3-030-91384-7/ebook). viii, 219 p. (2022).
Full Text:

### Verification, model checking, and abstract interpretation. 23rd International conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022. Proceedings. (English)Zbl 07496176

Lecture Notes in Computer Science 13182. Cham: Springer (ISBN 978-3-030-94582-4/pbk; 978-3-030-94583-1/ebook). x, 520 p. (2022).
MSC:  68-06 68Q60 00B25
Full Text:

Full Text:

### Mathematics and software verification. (English)Zbl 07481172

Heng, Liao (ed.) et al., Mathematics for future computing and communications. Cambridge: Cambridge University Press. 54-73 (2022).
Full Text:

### Dynamics of reputation in mobile agents systems and weighted timed automata. (English)Zbl 1483.68220

MSC:  68Q85 68Q45 68Q60
Full Text:

Full Text:

### Encoding safety in $$\mathrm{CLL}_R$$. (English)Zbl 07437213

MSC:  68Q85 03B44 68Q60
Full Text:

### Session-typed concurrent contracts. (English)Zbl 07432505

MSC:  68Q85 68N18 68Q60
Full Text:

### Metalevel transformation of strategies. (English)Zbl 07432502

MSC:  68Q60 68Q42
Full Text:

### Simulating and model checking membrane systems using strategies in Maude. (English)Zbl 07432501

MSC:  68Q07 68Q42 68Q60
Full Text:

### Formal verification of floating-point hardware design. A mathematical approach. 2nd edition. (English)Zbl 07414775

Cham: Springer (ISBN 978-3-030-87180-2/hbk; 978-3-030-87183-3/pbk; 978-3-030-87181-9/ebook). xxviii, 436 p. (2022).
MSC:  68-02 68M07 68Q60
Full Text:

### Parameterized verification of leader/follower systems via first-order temporal logic. (English)Zbl 07548213

MSC:  68Q60 03B44 68Q85
Full Text:

Full Text:

Full Text:

### Branching-time logics and fairness, revisited. (English)Zbl 07547345

MSC:  68Q60 03B44
Full Text:

### Proceedings of the 12th international symposium on games, automata, logics, and formal verification, GandALF, Padua, Italy, September 20–22, 2021. (English)Zbl 07544355

Electronic Proceedings in Theoretical Computer Science (EPTCS) 346. Waterloo: Open Publishing Association (OPA). 307 p., electronic only, open access (2021).
Full Text:

### Proceedings of the 37th international conference on logic programming (technical communications), ICLP, Porto, virtual event, September 20–27, 2021. (English)Zbl 07544354

Electronic Proceedings in Theoretical Computer Science (EPTCS) 345. Waterloo: Open Publishing Association (OPA). 309 p., electronic only, open access (2021).
MSC:  68-06 68Q60 00B25
Full Text:

### Proceedings of the 8th workshop on Horn clauses for verification and synthesis, HCVS, virtual, March 28, 2021. (English)Zbl 07544353

Electronic Proceedings in Theoretical Computer Science (EPTCS) 344. Waterloo: Open Publishing Association (OPA). 108 p., electronic only, open access (2021).
MSC:  68-06 68Q60 00B25
Full Text:

### Proceedings of the 9th international workshop on verification and program transformation, VPT, Luxembourg, Luxembourg, March 27–28, 2021. (English)Zbl 07544351

Electronic Proceedings in Theoretical Computer Science (EPTCS) 341. Waterloo: Open Publishing Association (OPA). 94 p., electronic only, open access (2021).
Full Text:

### Verifying graph programs with monadic second-order logic. (English)Zbl 07493665

Gadducci, Fabio (ed.) et al., Graph transformation. 14th international conference, ICGT 2021, held as part of STAF 2021, virtual event, June 24–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12741, 240-261 (2021).
Full Text:

### Interval probabilistic timed graph transformation systems. (English)Zbl 07493664

Gadducci, Fabio (ed.) et al., Graph transformation. 14th international conference, ICGT 2021, held as part of STAF 2021, virtual event, June 24–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12741, 221-239 (2021).
MSC:  68Q42 68Q60 68Q87
Full Text:

### Abstraction-based incremental inductive coverability for Petri nets. (English)Zbl 07493586

Buchs, Didier (ed.) et al., Application and theory of Petri nets and concurrency. 42nd international conference, PETRI NETS 2021, virtual event, June 23–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12734, 379-398 (2021).
MSC:  68Q85 68Q60 68W05
Full Text:

### A lazy query scheme for reachability analysis in Petri nets. (English)Zbl 07493585

Buchs, Didier (ed.) et al., Application and theory of Petri nets and concurrency. 42nd international conference, PETRI NETS 2021, virtual event, June 23–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12734, 360-378 (2021).
MSC:  68Q85 68Q60 68W05
Full Text:

### Efficient algorithms for three reachability problems in safe Petri nets. (English)Zbl 07493584

Buchs, Didier (ed.) et al., Application and theory of Petri nets and concurrency. 42nd international conference, PETRI NETS 2021, virtual event, June 23–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12734, 339-359 (2021).
MSC:  68Q85 68Q60 68W05
Full Text:

### Model checking of synchronized domain-specific multi-formalism models using high-level Petri nets. (English)Zbl 07493579

Buchs, Didier (ed.) et al., Application and theory of Petri nets and concurrency. 42nd international conference, PETRI NETS 2021, virtual event, June 23–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12734, 230-249 (2021).
MSC:  68Q60 68Q85
Full Text:

### Skeleton abstraction for universal temporal properties. (English)Zbl 07493577

Buchs, Didier (ed.) et al., Application and theory of Petri nets and concurrency. 42nd international conference, PETRI NETS 2021, virtual event, June 23–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12734, 186-207 (2021).
MSC:  68Q85 68Q60
Full Text:

### On the combination of polyhedral abstraction and SMT-based model checking for Petri nets. (English)Zbl 07493576

Buchs, Didier (ed.) et al., Application and theory of Petri nets and concurrency. 42nd international conference, PETRI NETS 2021, virtual event, June 23–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12734, 164-185 (2021).
MSC:  68Q85 68Q60
Full Text:

### Computing parameterized invariants of parameterized Petri nets. (English)Zbl 07493575

Buchs, Didier (ed.) et al., Application and theory of Petri nets and concurrency. 42nd international conference, PETRI NETS 2021, virtual event, June 23–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12734, 141-163 (2021).
MSC:  68Q85 68Q60
Full Text:

### Automatic synthesis of transiently correct network updates via Petri games. (English)Zbl 07493574

Buchs, Didier (ed.) et al., Application and theory of Petri nets and concurrency. 42nd international conference, PETRI NETS 2021, virtual event, June 23–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12734, 118-137 (2021).
Full Text:

### Canonical representations for direct generation of strategies in high-level Petri games. (English)Zbl 07493573

Buchs, Didier (ed.) et al., Application and theory of Petri nets and concurrency. 42nd international conference, PETRI NETS 2021, virtual event, June 23–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12734, 95-117 (2021).
MSC:  68Q85 68Q60 91A80
Full Text:

### A turn-based approach for qualitative time concurrent games. (English)Zbl 07493572

Buchs, Didier (ed.) et al., Application and theory of Petri nets and concurrency. 42nd international conference, PETRI NETS 2021, virtual event, June 23–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12734, 76-92 (2021).
MSC:  68Q85 68Q60 91A80
Full Text:

### Timed Petri nets with reset for pipelined synchronous circuit design. (English)Zbl 07493571

Buchs, Didier (ed.) et al., Application and theory of Petri nets and concurrency. 42nd international conference, PETRI NETS 2021, virtual event, June 23–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12734, 55-75 (2021).
Full Text:

### $$\pi$$ with leftovers: a mechanisation in Agda. (English)Zbl 07493477

Peters, Kirstin (ed.) et al., Formal techniques for distributed objects, components, and systems. 41st IFIP WG 6.1 international conference, FORTE 2021, held as part of the 16th international federated conference on distributed computing techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12719, 157-174 (2021).
Full Text:

Peters, Kirstin (ed.) et al., Formal techniques for distributed objects, components, and systems. 41st IFIP WG 6.1 international conference, FORTE 2021, held as part of the 16th international federated conference on distributed computing techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12719, 60-79 (2021).
Full Text:

### On bidirectional runtime enforcement. (English)Zbl 07493469

Peters, Kirstin (ed.) et al., Formal techniques for distributed objects, components, and systems. 41st IFIP WG 6.1 international conference, FORTE 2021, held as part of the 16th international federated conference on distributed computing techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12719, 3-21 (2021).
MSC:  68Q60 03B70 68Q85
Full Text:

### Automated technology for verification and analysis. 19th international symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021. Proceedings. (English)Zbl 07458676

Lecture Notes in Computer Science 12971. Cham: Springer (ISBN 978-3-030-88884-8/pbk; 978-3-030-88885-5/ebook). xv, 382 p. (2021).
MSC:  68-06 68Q60 00B25
Full Text:

### Verification of compliance for multilevel models in individual trace semantics. (English)Zbl 1485.68152

MSC:  68Q60 68Q55
Full Text:

Full Text:

Full Text:

### Opacity of networked discrete event systems. (English)Zbl 1475.68044

MSC:  68M25 68Q45 68Q60
Full Text:

### A theory of monitors. (English)Zbl 1475.68206

MSC:  68Q85 68Q60
Full Text:

### 28th international symposium on temporal representation and reasoning. TIME 2021, Klagenfurt, Austria (virtual conference), September 27–29, 2021. (English)Zbl 1473.68013

LIPIcs – Leibniz International Proceedings in Informatics 206. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik (ISBN 978-3-95977-206-8). xiv, 17 articles, not consecutively paged, electronic only, open access (2021).
Full Text:

### Fundamentals of logic and computation. With practical automated reasoning and verification. (English)Zbl 07420661

Texts in Computer Science. Cham: Springer (ISBN 978-3-030-87881-8/hbk; 978-3-030-87882-5/ebook). x, 221 p. (2021).
Full Text:

### Statistical model checking and time-bounded reachability analysis for hybrid Petri nets with multiple stochastic variables. (English)Zbl 1472.68003

Münster: Univ. Münster, Mathematisch-Naturwissenschaftliche Fakultät, Fachbereich Mathematik und Informatik (Diss.). xviii, 267 p. (2021).
MSC:  68-02 68Q60 68Q85

### Genmul: generating architecturally complex multipliers to challenge formal verification tools. (English)Zbl 07410746

Drechsler, Rolf (ed.) et al., Recent findings in Boolean techniques. Selected papers from the 14th international workshop on Boolean problems, IWSBP, virtual, September 24–25, 2020. Cham: Springer. 177-191 (2021).
MSC:  68Q60 68Q06 94C11
Full Text:

### Netter: probabilistic, stateful network models. (English)Zbl 1472.68012

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 486-508 (2021).
Full Text:

### Formal semantics and verification of network-based biocomputation circuits. (English)Zbl 1472.68057

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 464-485 (2021).
Full Text:

### A design of GPU-based quantitative model checking. (English)Zbl 1472.68091

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 441-463 (2021).
MSC:  68Q60 03B44 68N30
Full Text:

### A synchronous effects logic for temporal verification of pure Esterel. (English)Zbl 1472.68020

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 417-440 (2021).
MSC:  68N15 03B70 68Q60
Full Text:

### Syntax-guided synthesis for lemma generation in hardware model checking. (English)Zbl 1472.68096

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 325-349 (2021).
MSC:  68Q60 68M07
Full Text:

### Unbounded procedure summaries from bounded environments. (English)Zbl 1472.68093

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 291-324 (2021).
MSC:  68Q60 68N30
Full Text:

### Runtime abstract interpretation for numerical accuracy and robustness. (English)Zbl 1472.68095

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 243-266 (2021).
MSC:  68Q60 68N30
Full Text:

### A reduction theorem for randomized distributed algorithms under weak adversaries. (English)Zbl 1472.68083

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 219-239 (2021).
MSC:  68Q60 68W15 68W20
Full Text:

### Eliminating message counters in synchronous threshold automata. (English)Zbl 1472.68094

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 196-218 (2021).
MSC:  68Q60 68Q45 68W15
Full Text:

### Verification of concurrent programs using Petri net unfoldings. (English)Zbl 1472.68087

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 174-195 (2021).
MSC:  68Q60 68N19 68Q85
Full Text:

### Concurrent correctness in vector space. (English)Zbl 1472.68092

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 151-173 (2021).
MSC:  68Q60 68N19 68Q85
Full Text:

### A self-certifying compilation framework for WebAssembly. (English)Zbl 1472.68032

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 127-148 (2021).
MSC:  68N20 68Q60
Full Text:

### Proving the existence of fair paths in infinite-state systems. (English)Zbl 1472.68085

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 104-126 (2021).
MSC:  68Q60
Full Text:

### Decomposing data structure commutativity proofs with $$mn$$-differencing. (English)Zbl 1472.68090

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 81-103 (2021).
MSC:  68Q60 68P05
Full Text:

### Compositional model checking for multi-properties. (English)Zbl 1472.68089

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 55-80 (2021).
MSC:  68Q60
Full Text:

### Generative program analysis and beyond: the power of domain-specific languages (invited paper). (English)Zbl 1472.68042

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 29-51 (2021).
Full Text:

### Model checking algorithms for hyperproperties (invited paper). (English)Zbl 1472.68088

Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 3-16 (2021).
MSC:  68Q60 03B44 03D05
Full Text:

### Deductive verification of floating-point Java programs in KeY. (English)Zbl 1474.68186

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 242-261 (2021).
MSC:  68Q60 65G50 68N15
Full Text:

### cake_lpr: verified propagation redundancy checking in CakeML. (English)Zbl 1474.68194

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 223-241 (2021).
MSC:  68Q60 68V15
Full Text:

### An SMT-based approach for verifying binarized neural networks. (English)Zbl 1474.68188

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 203-222 (2021).
MSC:  68Q60 68T07 68T20
Full Text:

### Deductive stability proofs for ordinary differential equations. (English)Zbl 1474.68195

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 181-199 (2021).
Full Text:

### A two-phase approach for conditional floating-point verification. (English)Zbl 1474.68191

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 43-63 (2021).
MSC:  68Q60 65G50 68N30
Full Text:

### Directed reachability for infinite-state systems. (English)Zbl 1474.68202

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 3-23 (2021).
MSC:  68Q85 68Q60 68R10
Full Text:

### For a few dollars more. Verified fine-grained algorithm analysis down to LLVM. (English)Zbl 1473.68222

Yoshida, Nobuko (ed.), Programming languages and systems. 30th European symposium on programming, ESOP 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12648, 292-319 (2021).
MSC:  68W40 68P10 68Q60
Full Text:

### An automated deductive verification framework for circuit-building quantum programs. (English)Zbl 1473.68106

Yoshida, Nobuko (ed.), Programming languages and systems. 30th European symposium on programming, ESOP 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12648, 148-177 (2021).
Full Text:

### Verified software units. (English)Zbl 1473.68035

Yoshida, Nobuko (ed.), Programming languages and systems. 30th European symposium on programming, ESOP 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12648, 118-147 (2021).
Full Text:

### Checking robustness between weak transactional consistency models. (English)Zbl 1473.68063

Yoshida, Nobuko (ed.), Programming languages and systems. 30th European symposium on programming, ESOP 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12648, 87-117 (2021).
Full Text:

### The decidability of verification under PS 2.0. (English)Zbl 1474.68187

Yoshida, Nobuko (ed.), Programming languages and systems. 30th European symposium on programming, ESOP 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12648, 1-29 (2021).
MSC:  68Q60 68N30 68Q55
Full Text:

Full Text:

Full Text:

### Back-propagation through signal temporal logic specifications: infusing logical structure into gradient-based methods. (English)Zbl 1469.68127

Lavalle, Steven M. (ed.) et al., Algorithmic foundations of robotics XIV. Proceedings of the fourteenth workshop on the algorithmic foundations of robotics. Cham: Springer. Springer Proc. Adv. Robot. 17, 432-449 (2021).
MSC:  68T40 03B44 68Q60
Full Text:

### Spiking neural P systems: matrix representation and formal verification. (English)Zbl 1469.68035

MSC:  68Q07 68Q60 68Q85
Full Text:

### Accelerating predicate abstraction by minimum unsatisfiable cores extraction. (English)Zbl 1481.68032

He, Kun (ed.) et al., Theoretical computer science. 38th national conference, NCTCS 2020, Nanning, China, November 13–15, 2020. Revised selected papers. Singapore: Springer. Commun. Comput. Inf. Sci. 1352, 3-13 (2021).
MSC:  68Q60 03B70 68M07
Full Text:

### Model checking software. 27th international symposium, SPIN 2021, virtual event, July 12, 2021. Proceedings. (English)Zbl 1482.68029

Lecture Notes in Computer Science 12864. Cham: Springer (ISBN 978-3-030-84628-2/pbk; 978-3-030-84629-9/ebook). x, 195 p. (2021).
Full Text:

### Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part II. (English)Zbl 1482.68040

Lecture Notes in Computer Science 12760. Cham: Springer (ISBN 978-3-030-81687-2/pbk; 978-3-030-81688-9/ebook). xxiii, 940 p. (2021).
MSC:  68-06 68Q60 00B25
Full Text:

### Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part I. (English)Zbl 07386976

Lecture Notes in Computer Science 12759. Cham: Springer (ISBN 978-3-030-81684-1/pbk; 978-3-030-81685-8/ebook). xxiv, 922 p. (2021).
MSC:  68-06 68Q60 00B25
Full Text:

### Advances in verification of ReLU neural networks. (English)Zbl 1478.68172

MSC:  68Q60 68T07
Full Text:

### General decidability results for asynchronous shared-memory programs: higher-order and beyond. (English)Zbl 1467.68040

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12651, 449-467 (2021).
Full Text:

### Improving neural network verification through spurious region guided refinement. (English)Zbl 1467.68096

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12651, 389-408 (2021).
MSC:  68Q60 68T07
Full Text:

### Automated and formal synthesis of neural barrier certificates for dynamical models. (English)Zbl 1467.68091

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12651, 370-388 (2021).
MSC:  68Q60 68Q32 68T05
Full Text:

### Algebraic quantitative semantics for efficient online temporal monitoring. (English)Zbl 1467.68088

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12651, 330-348 (2021).
MSC:  68Q60 68Q55
Full Text:

### Timed automata relaxation for reachability. (English)Zbl 1467.68079

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12651, 291-310 (2021).
MSC:  68Q45 68Q60
Full Text:

### Multi-objective optimization of long-run average and total rewards. (English)Zbl 1467.68094

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12651, 230-249 (2021).
Full Text:

### Finding provably optimal Markov chains. (English)Zbl 1467.68095

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12651, 173-190 (2021).
MSC:  68Q60 60J22 68Q87
Full Text:

### Counterexample-guided prophecy for model checking modulo the theory of arrays. (English)Zbl 1467.68089

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12651, 113-132 (2021).
MSC:  68Q60
Full Text:

all top 5

all top 5

all top 5

all top 3

all top 3