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

Show other versions (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...

Bibliografske podrobnosti
Main Authors:	Horn, A, Kroening, D
Format:	Journal article
Jezik:	English
Izdano:	2015

Podobne knjige/članki

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

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

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

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

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

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

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

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

Automated concurrency bug finding using partial-orders
od: Horn, A
Izdano: (2015)

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

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

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

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

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

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

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

Concurrent logic games on partial orders
od: Gutierrez, J
Izdano: (2011)

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

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

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

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

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

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

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

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

Material Replenishment System For SMT Kitting
od: Ong, Xuan Zhi
Izdano: (2016)

Material Replenishment System For SMT Kitting
od: Ong, Xuan Zhi
Izdano: (2016)

SMT-Annual Meeting 2011 in Minneapolis
od: Jan Philipp Sprick
Izdano: (2011-01-01)

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

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

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

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

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

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

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

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

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

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

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

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