On the Complexity of the Correctness Problem for Non-Zeroness Test Instruction Sequences

This is to announce a new electronic preprint concerning instruction sequences. The paper entitled “On the complexity of the correctness problem for non-zeroness test instruction sequences” (arXiv:1805.05845v1 [cs.LO]) has now been archived. In this paper, we investigate the complexity of the problem of deciding whether a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction correctly implements the function modeling the non-zeroness test on natural numbers less than 2n with respect to their binary representation by bit strings of length n.

Advertisements
Posted in Announcement of Publication | Tagged , , , , , | Leave a comment

Axioms for Behavioural Congruence of Single-Pass Instruction Sequences

This is to announce the publication of a paper concerning instruction sequences. The paper entitled “Axioms for behavioural congruence of single-pass instruction sequences” (doi: 10.7561/SACS.2017.2.111) has now been published. This paper introduces a sound axiom system for behavioural congruence of single-pass instruction sequences that is complete for finite instruction sequences. This means that behavioural congruence of finite instruction sequences can now be established in a direct way by pure equational reasoning. In the past, it had to be established in an indirect way by reasoning that was not pure equational. The axiom system is especially notable for its axioms that have to do with forward jump instructions

Posted in Announcement of Publication | Tagged , , , , , , , | Leave a comment

Instruction Sequences Expressing Multiplication Algorithms

This is to announce an electronic preprint concerning instruction sequences, entitled “Instruction Sequences Expressing Multiplication Algorithms” (arXiv:1312.1529v3 [cs.PL]), in which “Instruction Sequence Expressions for the Karatsuba Multiplication Algorithm” (arXiv:1312.1529v2 [cs.PL]) has been combined with “Long Multiplication by Instruction Sequences with Backward Jump Instructions” (arXiv:1312.1812v3 [cs.PL]). In this preprint, we provide mathematically precise alternatives to the natural language and pseudo code descriptions of the long multiplication algorithm and the Karatsuba multiplication algorithm and establish among other things that the instruction sequence expressing the latter algorithm is shorter than the instruction sequence expressing the former algorithm only if the length of the bit strings involved is greater than 256. We also go into the use of an instruction sequence with backward jump instructions for expressing the long multiplication algorithm. This leads to an instruction sequence that it is shorter than the other two if the length of the bit strings involved is greater than 2.

Posted in Announcement of Publication | Tagged , , , , , , , , , , | Leave a comment

Axioms for Behavioural Congruence of Single-Pass Instruction Sequences

This is to announce a new version of an electronic preprint concerning instruction sequences. The paper entitled “Axioms for behavioural congruence of single-pass instruction sequences” (arXiv:1702.03511v2 [cs.PL]) has now been updated. This preprint introduces a sound axiom system for behavioural congruence of single-pass instruction sequences that is complete for finite instruction sequences. This means that behavioural congruence of finite instruction sequences can now be established in a direct way by pure equational reasoning. In the past, it had to be established in an indirect way by reasoning that was not pure equational. The axiom system is especially notable for its axioms that have to do with forward jump instructions.

Posted in Announcement of Publication | Tagged , , , , , , , | Leave a comment

Instruction Sequence Expressions for the Secure Hash Algorithm SHA-256

This is to announce a new version of an electronic preprint concerning instruction sequences. The preprint “Instruction Sequence Expressions for the Secure Hash Algorithm SHA-256” has now been updated (arXiv:1308.0219v7 [cs.PL]). In this preprint, we provide a mathematically precise alternatives to the pseudo code description of the secure hash algorithm SHA-256.

Posted in Announcement of Publication | Tagged , , , , , | Leave a comment

Instruction Sequence Expressions for the Karatsuba Multiplication Algorithm

This is to announce a new version of an electronic preprint concerning instruction sequences. The preprint “Instruction Sequence Expressions for the Karatsuba Multiplication Algorithm” has now been updated (arXiv:1312.1529v2 [cs.PL]). In this preprint, we provide mathematically precise alternatives to the natural language and pseudo code descriptions of the long multiplication algorithm and the Karatsuba multiplication algorithm and establish among other things that the instruction sequence expressing the latter algorithm is shorter than the instruction sequence expressing the former algorithm only if the length of the bit strings involved is greater than 256.

Posted in Announcement of Publication | Tagged , , , , , , , , | Leave a comment

A Hoare-Like Logic of Asserted Single-Pass Instruction Sequences

This is to announce the publication of a paper concerning instruction sequences. The paper entitled “A Hoare-like logic of asserted single-pass instruction sequences” (doi: 10.7561/SACS.2016.2.125) has now been published. In this paper, we present a Hoare-like logic that is intended to support a sound general understanding of the issues with Hoare-like logics for low-level programming languages.

Posted in Announcement of Publication | Tagged , , , , , , , , , | Leave a comment

Axioms for Behavioural Congruence of Single-Pass Instruction Sequences

This is to announce a new electronic preprint concerning instruction sequences. The paper entitled “Axioms for behavioural congruence of single-pass instruction sequences” (arXiv:1702.03511v1 [cs.PL]) has now been archived. This preprint introduces a sound axiom system for behavioural congruence of single-pass instruction sequences that is complete for finite instruction sequences. This means that behavioural congruence of finite instruction sequences can now be established in a direct way by pure equational reasoning. In the past, it had to be established in an indirect way by reasoning that was not pure equational.

Posted in Announcement of Publication | Tagged , , , , , , | Leave a comment

Instruction Sequence Size Complexity of Parity

This is to announce the publication of a paper concerning instruction sequences. The paper entitled “Instruction sequence size complexity of parity” (doi:10.3233/FI-2016-1450) has now been published. The main result of this paper supports, in a setting where programs are instruction sequences acting on Boolean registers, a basic intuition behind the storage of auxiliary data, namely the intuition that this makes possible a reduction of the size of a program.

Posted in Announcement of Publication | Tagged , , , , , , , | Leave a comment

On Instruction Sets for Boolean Registers in Program Algebra

This is to announce the publication of a paper concerning instruction sequences. The paper entitled “On instruction sets for Boolean registers in program algebra” (doi:10.7561/SACS.2016.1.1) has now been published. In this paper, we study instruction sequence size bounded functional completeness of instruction sets for Boolean registers.

Posted in Announcement of Publication | Tagged , , , , | Leave a comment