On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency

On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency

Mostra altre versioni (1)

Concurrent systems are notoriously difficult to analyze, and technological advances such as weak memory architectures greatly compound this problem. This has renewed interest in partial order semantics as a theoretical foundation for formal verification techniques. Among these, symbolic techniques h...

Descrizione completa

Dettagli Bibliografici
Autori principali:	Horn, A, Kroening, D
Natura:	Journal article
Lingua:	English
Pubblicazione:	2015

Documenti analoghi

On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency
di: Horn, A, et al.
Pubblicazione: (2015)

Efficient verification of concurrent systems using synchronisation analysis and SAT/SMT solving
di: Antonino, P, et al.
Pubblicazione: (2019)

An efficient SAT encoding of circuit codes
di: Chebiryak, Y, et al.
Pubblicazione: (2008)

A SAT−Based Algorithm for Reparameterization in Symbolic Simulation
di: Chauhan, P, et al.
Pubblicazione: (2004)

A SAT-based algorithm for reparameterization in symbolic simulation
di: Chauhan, P, et al.
Pubblicazione: (2004)

SAT and SMT-Based Verification of Security Protocols Including Time Aspects
di: Sabina Szymoniak, et al.
Pubblicazione: (2021-04-01)

Automatic generation of propagation complete SAT encodings
di: Brain, M, et al.
Pubblicazione: (2015)

Partial orders for efficient bounded model checking of concurrent software
di: Alglave, J, et al.
Pubblicazione: (2013)

Automated concurrency bug finding using partial-orders
di: Horn, A
Pubblicazione: (2015)

SMT Attack: Next Generation Attack on Obfuscated Circuits with Capabilities and Performance Beyond the SAT Attacks
di: Kimia Zamiri Azar, et al.
Pubblicazione: (2018-11-01)

Modular strategic SMT solving with SMT-RAT
di: Kremer Gereon, et al.
Pubblicazione: (2018-08-01)

The order encoding: from tractable CSP to tractable SAT
di: Petke, J, et al.
Pubblicazione: (2011)

The order encoding: From tractable CSP to tractable SAT
di: Petke, J, et al.
Pubblicazione: (2011)

SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME
di: A. Niewiadomski, et al.
Pubblicazione: (2018-12-01)

Language and Proofs for Higher-Order SMT (Work in Progress)
di: Haniel Barbosa, et al.
Pubblicazione: (2017-12-01)

The order encoding: from tractable CSP to tractable SAT (extended abstract)
di: Petke, J, et al.
Pubblicazione: (2011)

Concurrent logic games on partial orders
di: Gutierrez, J
Pubblicazione: (2011)

ExpliSAT: Guiding SAT−Based Software Verification with Explicit States
di: Barner, S, et al.
Pubblicazione: (2007)

REINFORCED ENCODING FOR PLANNING AS SAT
di: Tomáš Balyo, et al.
Pubblicazione: (2015-12-01)

Correctness of Concurrent Objects under Weak Memory Models
di: Graeme Smith, et al.
Pubblicazione: (2018-10-01)

Encoding floating-points using the SMT theory in ESBMC: An empirical evaluation over the SV-COMP benchmarks
di: Gadelha, M, et al.
Pubblicazione: (2017)

SAT−based Summarisation for Boolean Programs
di: Basler, G, et al.
Pubblicazione: (2007)

Unfolding-based partial order reduction
di: Rodríguez, C, et al.
Pubblicazione: (2015)

Software Verification for Weak Memory via Program Transformation
di: Alglave, J, et al.
Pubblicazione: (2013)

Software verification for weak memory via program transformation
di: Alglave, J, et al.
Pubblicazione: (2013)

Material Replenishment System For SMT Kitting
di: Ong, Xuan Zhi
Pubblicazione: (2016)

Material Replenishment System For SMT Kitting
di: Ong, Xuan Zhi
Pubblicazione: (2016)

SMT-Annual Meeting 2011 in Minneapolis
di: Jan Philipp Sprick
Pubblicazione: (2011-01-01)

Homologi Gen Seleno Metiltransferase (smt) pada Geobacillus sp. 20k dengan smt Astragalus bisulcatus
di: Evi Triana, et al.
Pubblicazione: (2010-09-01)

Stream−based Randomised Language Models for SMT
di: Levenberg, A, et al.
Pubblicazione: (2009)

Soundness of Data Flow Analyses for Weak Memory Models
di: Alglave, J, et al.
Pubblicazione: (2011)

Soundness of data flow analyses for weak memory models
di: Alglave, J, et al.
Pubblicazione: (2011)

Soundness of Data Flow Analyses for Weak Memory Models
di: Alglave, J, et al.
Pubblicazione: (2011)

TOWARDS SEMANTIC ENCODING IN DIGITAL PATHOLOGY USING WEAKLY SUPERVISED LEARNING STRATEGIES
di: Alexander Baras, et al.
Pubblicazione: (2022-01-01)

SATABS: SAT−based Predicate Abstraction for ANSI−C
di: Clarke, E, et al.
Pubblicazione: (2005)

CELESTICA SUMBANG SMT LENGKAP KEPADA USM
di: MPRC, Pusat Media & Perhubungan Awam
Pubblicazione: (2015)

SMT defect reduction using DMAIC methodology /
di: L. Thiruvarasu Letchumanan, 1980-, et al.
Pubblicazione: (2009)

Reasoning with Finite Sets and Cardinality Constraints in SMT
di: Kshitij Bansal, et al.
Pubblicazione: (2018-11-01)

表面安装技术（SMT）应用简介
di: 汤大伦
Pubblicazione: (1994-01-01)

Predicting SMT Solver Performance for Software Verification
di: Andrew Healy, et al.
Pubblicazione: (2017-01-01)