Game semantics based equivalence checking of higher-order programs

Game semantics based equivalence checking of higher-order programs

Taispeáin leaganacha eile (1)

<p>This thesis examines the use of game semantics for the automatic equivalence checking of higher-order programs. Game semantics has proved to be a powerful method for constructing fully abstract models of logics and programming languages. Furthermore, the concrete nature of the semantics...

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí:	Hopkins, D, David Hopkins
Rannpháirtithe:	Ong, C
Formáid:	Tráchtas
Teanga:	English
Foilsithe / Cruthaithe:	2012
Ábhair:	Theory and automated verification Game semantics

Míreanna comhchosúla

Game Semantics Based Equivalence Checking of Higher−Order Programs
de réir: Hopkins, D
Foilsithe / Cruthaithe: (2012)

Functions with local state: regularity and undecidability
de réir: Murawski, A
Foilsithe / Cruthaithe: (2005)

Intersection types and higer-order model checking
de réir: Ramsay, S, et al.
Foilsithe / Cruthaithe: (2014)

Higher-order semantics for quantum programming languages with classical control
de réir: Atzemoglou, GP
Foilsithe / Cruthaithe: (2012)

Abstraction discovery and refinement for model checking by symbolic trajectory evaluation
de réir: Adams, S
Foilsithe / Cruthaithe: (2014)

Precise verification of C programs
de réir: Lewis, M
Foilsithe / Cruthaithe: (2014)

Mean-Payoff Games with <i>ω</i>-Regular Specifications
de réir: Julian Gutierrez, et al.
Foilsithe / Cruthaithe: (2022-02-01)

Games for complexity of second-order call-by-name programs
de réir: Murawski, A
Foilsithe / Cruthaithe: (2005)

Automated quantitative software verification
de réir: Kattenbelt, M
Foilsithe / Cruthaithe: (2010)

Forward looking logics and automata
de réir: Ley, C
Foilsithe / Cruthaithe: (2011)

Probabilistic guarded commands mechanized in HOL
de réir: Hurd, J, et al.
Foilsithe / Cruthaithe: (2005)

Incremental modelling for verified communication architectures
de réir: Boehm, P, et al.
Foilsithe / Cruthaithe: (2011)

Homer: A Higher−order Observational equivalence Model checkER
de réir: Hopkins, D, et al.
Foilsithe / Cruthaithe: (2009)

Digraph measures: Kelly decompositions, games, and orderings
de réir: Hunter, P, et al.
Foilsithe / Cruthaithe: (2008)

Partial correctness for probabilistic demonic programs
de réir: McIver, A, et al.
Foilsithe / Cruthaithe: (2001)

Saturation methods for global model-checking pushdown systems
de réir: Hague, M
Foilsithe / Cruthaithe: (2009)

THE PRESENT STATE OF THE INFORMATION-MEASURING SYSTEMS FOR CHECKING HIGH VOLTAGE CONVERTERS
de réir: A.S. Ilin, et al.
Foilsithe / Cruthaithe: (2022-12-01)

Time effect of stimulus exposure in semantic verification task
de réir: Injac Božana, et al.
Foilsithe / Cruthaithe: (2006-01-01)

An algebraic theory of componentised interaction
de réir: Chilton, C
Foilsithe / Cruthaithe: (2013)

EXK-SC: A Semantic Communication Model Based on Information Framework Expansion and Knowledge Collision
de réir: Gangtao Xin, et al.
Foilsithe / Cruthaithe: (2022-12-01)

Automatic C Program Verification Based on Mixed Axiomatic Semantics
de réir: I. V. Maryasov, et al.
Foilsithe / Cruthaithe: (2013-12-01)

Equivalence of the schemes of programs based on the algebraic approach to setting the semantics of programming languages
de réir: Y. P. Korablin
Foilsithe / Cruthaithe: (2022-03-01)

On the equivalence between non-factorizable mixed-strategy classical games and quantum games
de réir: Azhar Iqbal, et al.
Foilsithe / Cruthaithe: (2016-01-01)

An interpolating decision procedure for transitive relations with uninterpreted functions
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2009)

Program analysis with interpolants
de réir: Weissenbacher, G, et al.
Foilsithe / Cruthaithe: (2010)

Neural mechanisms underlying the facilitation of naming in aphasia using a semantic task: an fMRI study
de réir: Heath Shiree, et al.
Foilsithe / Cruthaithe: (2012-08-01)

GTIP: A Gaming-Based Topic Influence Percolation Model for Semantic Overlapping Community Detection
de réir: Hailu Yang, et al.
Foilsithe / Cruthaithe: (2022-09-01)

Extensible hierarchical codec semantic communication system
de réir: Yuyuan ZHANG, et al.
Foilsithe / Cruthaithe: (2023-08-01)

Extensible hierarchical codec semantic communication system
de réir: Yuyuan ZHANG, et al.
Foilsithe / Cruthaithe: (2023-08-01)

Repairing strings and trees
de réir: Riveros Jaeger, C
Foilsithe / Cruthaithe: (2013)

Quantitative verification of real-time properties with application to medical devices
de réir: Marco Diciolla, M, et al.
Foilsithe / Cruthaithe: (2014)

Computer Games as Virtual Environments for Safety-Critical Software Validation
de réir: Štefan Korečko, et al.
Foilsithe / Cruthaithe: (2017-12-01)

Predicate Abstraction of ANSI-C Programs Using SAT
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2004)

A reversed form of public goods game: equivalence and difference
de réir: Chaoqian Wang, et al.
Foilsithe / Cruthaithe: (2022-01-01)

Coinductive Natural Semantics for Compiler Verification in Coq
de réir: Angel Zúñiga, et al.
Foilsithe / Cruthaithe: (2020-09-01)

Optimization of Window Size for Calculating Semantic Coherence Within an Essay
de réir: Kshitiz Srivastava, et al.
Foilsithe / Cruthaithe: (2022-10-01)

Abstract satisfaction
de réir: Haller, L
Foilsithe / Cruthaithe: (2013)

Program synthesis from domain specific object models
de réir: Faitelson, D
Foilsithe / Cruthaithe: (2008)

SMT-Based Consistency Checking of Configuration-Based Components Specifications
de réir: Laura Pandolfo, et al.
Foilsithe / Cruthaithe: (2021-01-01)

Central limit model checking
de réir: Bortolussi, L, et al.
Foilsithe / Cruthaithe: (2018)