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

Показать другие версии (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...

Полное описание

Библиографические подробности
Главные авторы:	Horn, A, Kroening, D
Формат:	Journal article
Язык:	English
Опубликовано:	2015

Схожие документы

On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency
по: Horn, A, и др.
Опубликовано: (2015)

Efficient verification of concurrent systems using synchronisation analysis and SAT/SMT solving
по: Antonino, P, и др.
Опубликовано: (2019)

An efficient SAT encoding of circuit codes
по: Chebiryak, Y, и др.
Опубликовано: (2008)

A SAT−Based Algorithm for Reparameterization in Symbolic Simulation
по: Chauhan, P, и др.
Опубликовано: (2004)

A SAT-based algorithm for reparameterization in symbolic simulation
по: Chauhan, P, и др.
Опубликовано: (2004)

SAT and SMT-Based Verification of Security Protocols Including Time Aspects
по: Sabina Szymoniak, и др.
Опубликовано: (2021-04-01)

Automatic generation of propagation complete SAT encodings
по: Brain, M, и др.
Опубликовано: (2015)

Partial orders for efficient bounded model checking of concurrent software
по: Alglave, J, и др.
Опубликовано: (2013)

Automated concurrency bug finding using partial-orders
по: Horn, A
Опубликовано: (2015)

SMT Attack: Next Generation Attack on Obfuscated Circuits with Capabilities and Performance Beyond the SAT Attacks
по: Kimia Zamiri Azar, и др.
Опубликовано: (2018-11-01)

Modular strategic SMT solving with SMT-RAT
по: Kremer Gereon, и др.
Опубликовано: (2018-08-01)

The order encoding: from tractable CSP to tractable SAT
по: Petke, J, и др.
Опубликовано: (2011)

The order encoding: From tractable CSP to tractable SAT
по: Petke, J, и др.
Опубликовано: (2011)

SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME
по: A. Niewiadomski, и др.
Опубликовано: (2018-12-01)

Language and Proofs for Higher-Order SMT (Work in Progress)
по: Haniel Barbosa, и др.
Опубликовано: (2017-12-01)

The order encoding: from tractable CSP to tractable SAT (extended abstract)
по: Petke, J, и др.
Опубликовано: (2011)

Concurrent logic games on partial orders
по: Gutierrez, J
Опубликовано: (2011)

ExpliSAT: Guiding SAT−Based Software Verification with Explicit States
по: Barner, S, и др.
Опубликовано: (2007)

REINFORCED ENCODING FOR PLANNING AS SAT
по: Tomáš Balyo, и др.
Опубликовано: (2015-12-01)

Correctness of Concurrent Objects under Weak Memory Models
по: Graeme Smith, и др.
Опубликовано: (2018-10-01)

Encoding floating-points using the SMT theory in ESBMC: An empirical evaluation over the SV-COMP benchmarks
по: Gadelha, M, и др.
Опубликовано: (2017)

SAT−based Summarisation for Boolean Programs
по: Basler, G, и др.
Опубликовано: (2007)

Unfolding-based partial order reduction
по: Rodríguez, C, и др.
Опубликовано: (2015)

Software Verification for Weak Memory via Program Transformation
по: Alglave, J, и др.
Опубликовано: (2013)

Software verification for weak memory via program transformation
по: Alglave, J, и др.
Опубликовано: (2013)

Material Replenishment System For SMT Kitting
по: Ong, Xuan Zhi
Опубликовано: (2016)

Material Replenishment System For SMT Kitting
по: Ong, Xuan Zhi
Опубликовано: (2016)

SMT-Annual Meeting 2011 in Minneapolis
по: Jan Philipp Sprick
Опубликовано: (2011-01-01)

Homologi Gen Seleno Metiltransferase (smt) pada Geobacillus sp. 20k dengan smt Astragalus bisulcatus
по: Evi Triana, и др.
Опубликовано: (2010-09-01)

Stream−based Randomised Language Models for SMT
по: Levenberg, A, и др.
Опубликовано: (2009)

Soundness of Data Flow Analyses for Weak Memory Models
по: Alglave, J, и др.
Опубликовано: (2011)

Soundness of data flow analyses for weak memory models
по: Alglave, J, и др.
Опубликовано: (2011)

Soundness of Data Flow Analyses for Weak Memory Models
по: Alglave, J, и др.
Опубликовано: (2011)

TOWARDS SEMANTIC ENCODING IN DIGITAL PATHOLOGY USING WEAKLY SUPERVISED LEARNING STRATEGIES
по: Alexander Baras, и др.
Опубликовано: (2022-01-01)

SATABS: SAT−based Predicate Abstraction for ANSI−C
по: Clarke, E, и др.
Опубликовано: (2005)

CELESTICA SUMBANG SMT LENGKAP KEPADA USM
по: MPRC, Pusat Media & Perhubungan Awam
Опубликовано: (2015)

SMT defect reduction using DMAIC methodology /
по: L. Thiruvarasu Letchumanan, 1980-, и др.
Опубликовано: (2009)

Reasoning with Finite Sets and Cardinality Constraints in SMT
по: Kshitij Bansal, и др.
Опубликовано: (2018-11-01)

表面安装技术（SMT）应用简介
по: 汤大伦
Опубликовано: (1994-01-01)

Predicting SMT Solver Performance for Software Verification
по: Andrew Healy, и др.
Опубликовано: (2017-01-01)