Demonstration venue · read-only. Every page can be browsed; the buttons that would change it are switched off. Create an account to run TaxoReview on your own data. A simulation from public publication records: the people listed were not invited and did not agree to review.

James C. King

dblp:92/1703 · DBLP profile ↗
← Back
5ranked-venue papers
5as first author
0since 2021 · last 1980
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 2 · 2 first-authorTheory of computation · 2 · 2 first-authorSystems, architecture and hardware · 1 · 1 first-author

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Software engineering, system software, and programming languages
4 papers
Program verification · 90% Programming languages and type systems · 10%
Theoretical computer science
2 papers
Logic in computer science · 89% Automated reasoning and model checking · 11%

Topics — the 7 heaviest of 8, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Program verification › invariant generation
inductive assertions
0.011980
Program Correctness: On Inductive Assertion Methods · IEEE Trans. Software Eng. 1980
Logic in computer science
program semantics
0.011980
Program Correctness: On Inductive Assertion Methods · IEEE Trans. Software Eng. 1980
Logic in computer science › semantics
relational semantics
0.011980
Program Correctness: On Inductive Assertion Methods · IEEE Trans. Software Eng. 1980
Program verification
correctness proof
0.011971
Proving Programs to be Correct · IEEE Trans. Computers 1971
Programming languages and type systems
language semantics
0.011971
Proving Programs to be Correct · IEEE Trans. Computers 1971
Program verification
predicate transformers
0.011980
Program Correctness: On Inductive Assertion Methods · IEEE Trans. Software Eng. 1980
Automated reasoning and model checking
theorem proving
0.011970
An Interpretation Oriented Theorem Prover over Integers · STOC 1970

Methods — techniques the papers use, named apart from their topics

subgoal induction · 0.0inductive assertions · 0.0formal correctness proof · 0.0expression simplification · 0.0
YearPublicationVenuePosition
1980 Program Correctness: On Inductive Assertion Methods
abstract
A study of several of the proof of correctness methods is presented. In particular, the form of induction used is explored in detail. A relational semantic model for programming languages is introduced and its relation to predicate transformers is explored. A rather elementary viewpoint is taken in order to expose, as simply as possible, the basic differences of the methods and the underlying principles involved. These results were obtained by attempting to thoroughly understand the "subgoal induction" method.
James C. King
IEEE Trans. Software Eng.1
1978 Prospects for Program Verification (Tutorial)
James C. King
ICSE1
1972 An Interpretation-Oriented Theorem Prover over Integers
James C. King, Robert W. Floyd
J. Comput. Syst. Sci.1
1971 Proving Programs to be Correct
abstract
This paper formally describes a technique for proving that computer programs will always execute correctly. In order to do this, an abstract model for a program and its execution is given. Then, correctness of programs and proofs of correctness of programs are defined with respect to that model.
James C. King
IEEE Trans. Computers1
1970 An Interpretation Oriented Theorem Prover over Integers
abstract
A special purpose theorem prover for establishing the validity of expressions over integer variables was developed as part of a program verifier. It is built around a powerful system for manipulating and simplifying integer expressions.
James C. King, Robert W. Floyd
STOC1