Π€ΠΎΡΠΌΠ°Π»ΡΠ½Π°Ρ ΡΠ΅ΠΌΠ°Π½ΡΠΈΠΊΠ° C-LIGHT ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ ΠΈ ΠΈΡ Π²Π΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΡ ΠΌΠ΅ΡΠΎΠ΄ΠΎΠΌ Π₯ΠΎΠ°ΡΠ°
ΠΠΈΡΡΠ΅ΡΡΠ°ΡΠΈΡ
ΠΠ°ΠΊ ΠΈΠ·Π²Π΅ΡΡΠ½ΠΎ, Π²ΡΠ±ΠΎΡ ΡΠ΅ΠΌΠ°Π½ΡΠΈΠΊΠΈ Π΄Π»Ρ ΠΊΠΎΠ½ΡΡΡΡΠΊΡΠΈΠΉ ΡΠ·ΡΠΊΠ° ΡΡΠ°Π½ΠΎΠ²ΠΈΡΡΡ ΡΠ΅ΡΠ°ΡΡΠΈΠΌ ΡΠ°ΠΊΡΠΎΡΠΎΠΌ Π΄Π»Ρ ΡΠ»ΠΎΠΆΠ½ΠΎΡΡΠΈ Π²Π΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΠΈ. Π Π½Π°ΡΡΠΎΡΡΠ΅Π΅ Π²ΡΠ΅ΠΌΡ Π½Π°ΠΈΠ±ΠΎΠ»Π΅Π΅ ΠΏΠΎΠΏΡΠ»ΡΡΠ½Ρ ΠΎΠΏΠ΅ΡΠ°ΡΠΈΠΎΠ½Π½ΡΠΉ ΠΈ Π°ΠΊΡΠΈΠΎΠΌΠ°ΡΠΈΡΠ΅ΡΠΊΠΈΠΉ ΠΏΠΎΠ΄Ρ ΠΎΠ΄Ρ. ΠΠ΅ΡΠ²ΡΠΉ Ρ ΠΎΡΠΎΡΠΎ ΠΏΠΎΠ΄Ρ ΠΎΠ΄ΠΈΡ Π΄Π»Ρ ΡΠΎΡΠΌΠ°Π»ΡΠ½ΠΎΠ³ΠΎ ΠΎΠΏΠΈΡΠ°Π½ΠΈΡ ΠΈΡΠΏΠΎΠ»Π½Π΅Π½ΠΈΡ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ Π½Π΅ΠΊΠΎΡΠΎΡΡΠΌ Π°Π±ΡΡΡΠ°ΠΊΡΠ½ΡΠΌ ΠΈΠ½ΡΠ΅ΡΠΏΡΠ΅ΡΠ°ΡΠΎΡΠΎΠΌ, ΡΡΠΎ ΠΏΠΎΠ·Π²ΠΎΠ»ΡΠ΅Ρ ΠΌΠΎΠ΄Π΅Π»ΠΈΡΠΎΠ²Π°ΡΡ ΡΠ΅Π°Π»ΡΠ½ΠΎΠ΅ ΠΏΠΎΠ²Π΅Π΄Π΅Π½ΠΈΠ΅ Π² ΠΊΠΎΠ½ΠΊΡΠ΅ΡΠ½ΡΡ ΡΠΈΡΡΠ΅ΠΌΠ°Ρ . ΠΠ΄Π½Π°ΠΊΠΎ ΠΏΠΎΠΏΡΡΠΊΠΈ Π²Π΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΠΈ… Π§ΠΈΡΠ°ΡΡ Π΅ΡΡ >
Π‘ΠΏΠΈΡΠΎΠΊ Π»ΠΈΡΠ΅ΡΠ°ΡΡΡΡ
- ΠΠ³Π°ΡΠΎΠ½ΠΎΠ² Π.Π. Π‘ΠΏΠ΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΡ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ: ΠΏΠΎΠ½ΡΡΠΈΠΉΠ½ΡΠ΅ ΡΡΠ΅Π΄ΡΡΠ²Π° ΠΈ ΠΈΡ ΠΎΡΠ³Π°Π½ΠΈΠ·Π°ΡΠΈΡ. — ΠΠΎΠ²ΠΎΡΠΈΠ±ΠΈΡΡΠΊ: ΠΠ°ΡΠΊΠ°, 1987. — 240 Ρ.
- ΠΠΎΡΠΊΠΎΠ² Π‘.Π., Π‘ΡΠ±Π±ΠΎΡΠΈΠ½ Π. Π. Π―Π·ΡΠΊ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΡ Π‘ΠΈ Π΄Π»Ρ ΠΏΠ΅ΡΡΠΎΠ½Π°Π»ΡΠ½ΠΎΠ³ΠΎ ΠΊΠΎΠΌΠΏΡΡΡΠ΅ΡΠ°. — Π.: Π Π°Π΄ΠΈΠΎ ΠΈ ΡΠ²ΡΠ·Ρ, 1990. — 384 Ρ.
- ΠΠΈΡΡ Π. ΠΠ»Π³ΠΎΡΠΈΠΌΡ ΠΈ ΡΡΡΡΠΊΡΡΡΡ Π΄Π°Π½Π½ΡΡ . — Π.: ΠΠΈΡ, 1989. — 360 Ρ.
- ΠΠ»ΡΡΠΊΠΎΠ² Π.Π. Π’Π΅ΠΎΡΠΈΡ Π°Π²ΡΠΎΠΌΠ°ΡΠΎΠ² ΠΈ ΡΠΎΡΠΌΠ°Π»ΡΠ½ΡΠ΅ ΠΏΡΠ΅ΠΎΠ±ΡΠ°Π·ΠΎΠ²Π°Π½ΠΈΡ ΠΌΠΈΠΊΡΠΎΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ // ΠΠΈΠ±Π΅ΡΠ½Π΅ΡΠΈΠΊΠ°. 1965. — N 5. — Π‘. 1−9.
- ΠΡΠΈΡ Π. ΠΠ°ΡΠΊΠ° ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΡ. — Π.: ΠΠΈΡ, 1984. — 416 Ρ.
- ΠΠ΅ΠΉΠΊΡΡΡΠ° Π. ΠΠΈΡΡΠΈΠΏΠ»ΠΈΠ½Π° ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΡ. — Π.: ΠΠΈΡ, 1978. — 275 Ρ.
- ΠΡΡΠΎΠ² Π.Π. ΠΠ·Π±ΡΠ°Π½Π½ΡΠ΅ ΡΡΡΠ΄Ρ / ΠΡΠ². ΡΠ΅Π΄. Π. Π. ΠΠΎΡΡΠΎΡΠΈΠ½. — ΠΠΎΠ²ΠΎΡΠΈΠ±ΠΈΡΡΠΊ: ΠΠ°ΡΠΊΠ°, 1994. 416 Ρ.
- ΠΡΡΠΎΠ² Π.Π., ΠΡΠΏΡΠ½ΠΎΠ² Π. Π. Π ΡΠΎΡΠΌΠ°Π»ΠΈΠ·Π°ΡΠΈΠΈ ΠΏΠΎΠ½ΡΡΠΈΡ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΡ // ΠΠΈΠ±Π΅ΡΠ½Π΅ΡΠΈΠΊΠ°. 1967. — N 5. — Π‘. 40−57.
- ΠΠ°ΠΌΡΠ»ΠΈΠ½ Π.Π. Π€ΠΎΡΠΌΠ°Π»ΡΠ½ΡΠ΅ ΠΌΠ΅ΡΠΎΠ΄Ρ ΡΠΏΠ΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΠΈ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ (Π£ΡΠ΅Π±Π½ΠΎΠ΅ ΠΏΠΎΡΠΎΠ±ΠΈΠ΅). — ΠΠΎΠ²ΠΈΡΠΈΠ±ΠΈΡΡΠΊ: ΠΠΠ£, 1999. —81 Ρ.
- ΠΠ°ΠΌΡΠ»ΠΈΠ½ Π.Π. Π€ΠΎΡΠΌΠ°Π»ΡΠ½Π°Ρ ΡΠ΅ΠΌΠ°Π½ΡΠΈΠΊΠ° Π²ΡΡΠ°ΠΆΠ΅Π½ΠΈΠΉ ΠΈ ΠΎΠΏΠ΅ΡΠ°ΡΠΎΡΠΎΠ² ΡΠ·ΡΠΊΠ° Java // ΠΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΠ΅. — 2003. — N 5. — Π‘. 31−45.
- ΠΠ°ΠΌΡΠ»ΠΈΠ½ Π.Π. ΠΠ»Π³Π΅ΡΠ°ΠΈΡΠ΅ΡΠΊΠ°Ρ ΡΠ΅ΠΌΠ°Π½ΡΠΈΠΊΠ° ΠΈΠΌΠΏΠ΅ΡΠ°ΡΠΈΠ²Π½ΠΎΠ³ΠΎ ΡΠ·ΡΠΊΠ° ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΡ // ΠΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΠ΅. — 2003. — N 6. — Π‘. 51−64.
- ΠΠ΅ΡΠ½ΠΈΠ³Π°Π½ Π., Π ΠΈΡΡΠΈ Π. Π―Π·ΡΠΊ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΡ Π‘ΠΈ. — Π.: Π€ΠΈΠ½Π°Π½ΡΡ ΠΈ ΡΡΠ°ΡΠΈΡΡΠΈΠΊΠ°, 1985.
- ΠΠΎΡΠΎΠ² Π.Π., Π‘Π°Π±Π΅Π»ΡΡΠ΅Π»ΡΠ΄ Π. Π. Π’Π΅ΠΎΡΠΈΡ ΡΡ Π΅ΠΌ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ. — Π.: ΠΠ°ΡΠΊΠ°. ΠΠ». ΡΠ΅Π΄. ΡΠΈΠ·.-ΠΌΠ°Ρ. Π»ΠΈΡ., 1991. — 248 Ρ.
- ΠΠ°Π²ΡΠΎΠ² Π‘.Π‘. ΠΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΠ΅. ΠΠ°ΡΠ΅ΠΌΠ°ΡΠΈΡΠ΅ΡΠΊΠΈΠ΅ ΠΎΡΠ½ΠΎΠ²Ρ, ΡΡΠ΅Π΄ΡΡΠ²Π°, ΡΠ΅ΠΎΡΠΈΡ. — Π‘ΠΠ±.: ΠΠ₯Π-ΠΠ΅ΡΠ΅ΡΠ±ΡΡΠ³, 2001. 320 Ρ.
- ΠΠ΅ΡΠΈΡΠ΅Π²ΡΠΊΠΈΠΉ Π.Π. Π‘ΠΈΠ½ΡΠ°ΠΊΡΠΈΡ ΠΈ ΡΠ΅ΠΌΠ°Π½ΡΠΈΠΊΠ° ΡΠΎΡΠΌΠ°Π»ΡΠ½ΡΡ ΡΠ·ΡΠΊΠΎΠ² // ΠΠΈΠ±Π΅ΡΠ½Π΅ΡΠΈΠΊΠ°.- 1968. N 4. — Π‘. 1−9.
- ΠΠ΅ΡΠΈΡΠ΅Π²ΡΠΊΠΈΠΉ Π.Π. ΠΠΊΠ²ΠΈΠ²Π°Π»Π΅Π½ΡΠ½ΠΎΡΡΡ ΠΈ ΠΎΠΏΡΠΈΠΌΠΈΠ·Π°ΡΠΈΡ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ // Π’Π΅ΠΎΡΠΈΡ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΡ. — ΠΠΎΠ²ΠΎΡΠΈΠ±ΠΈΡΡΠΊ, 1972. — Π§. 1. — Π‘. 166−180.
- ΠΠ°ΠΉΠ΅ΡΡ Π. ΠΡΠΊΡΡΡΡΠ²ΠΎ ΡΠ΅ΡΡΠΈΡΠΎΠ²Π°Π½ΠΈΡ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ. — Π.: Π€ΠΈΠ½Π°Π½ΡΡ ΠΈ ΡΡΠ°ΡΠΈΡΡΠΈΠΊΠ°, 1982.- 176 Ρ.
- ΠΠ°ΡΡΠ΅Ρ Π. Π‘ΠΏΠ΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΡ Π°Π±ΡΡΡΠ°ΠΊΡΠ½ΡΡ ΡΠΈΠΏΠΎΠ² Π΄Π°Π½Π½ΡΡ Π² ΡΠΈΡΡΠ΅ΠΌΠ΅ AFFIRM // Π’ΡΠ΅Π±ΠΎΠ²Π°Π½ΠΈΡ ΠΈ ΡΠΏΠ΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΠΈ Π² ΡΠ°Π·ΡΠ°Π±ΠΎΡΠΊΠ΅ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ. — Π.: ΠΠΈΡ, 1984. — Π‘. 199—222.
- ΠΠ΅ΠΏΠ΅ΠΉΠ²ΠΎΠ΄Π° Π. Π., Π‘ΠΊΠΎΠΏΠΈΠ½ Π. Π. ΠΡΠ½ΠΎΠ²Π°Π½ΠΈΡ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΡ. — ΠΠΆΠ΅Π²ΡΠΊ-ΠΠΎΡΠΊΠ²Π°: Π Π₯Π, 2003. 926 Ρ.
- ΠΠ΅ΠΏΠΎΠΌΠ½ΡΡΠΈΠΉ Π.Π. ΠΠ± ΠΎΠ΄Π½ΠΎΠΌ ΠΌΠ΅ΡΠΎΠ΄Π΅ ΡΠ°ΡΠΏΠΎΠ·Π½Π°Π²Π°Π½ΠΈΡ ΡΠΊΠ²ΠΈΠ²Π°Π»Π΅Π½ΡΠ½ΠΎΡΡΠΈ ΡΡ Π΅ΠΌ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ ΠΈ Π΄ΠΈΡΠΊΡΠ΅ΡΠ½ΡΡ ΠΏΡΠ΅ΠΎΠ±ΡΠ°Π·ΠΎΠ²Π°ΡΠ΅Π»Π΅ΠΉ // Π’ΡΡΠ΄Ρ ΠΡΠ΅ΡΠΎΡΠ·. ΠΊΠΎΠ½Ρ. ΠΏΠΎ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΡ (ΠΠΠ-2). ΠΠΎΠ²ΠΎΡΠΈΠ±ΠΈΡΡΠΊ, 1970. — ΠΡΠΏ. Π. — Π‘. 49−63.
- ΠΠ΅ΠΏΠΎΠΌΠ½ΡΡΠΈΠΉ Π.Π. Π ΠΏΡΠΎΠ±Π»Π΅ΠΌΠ½ΠΎ-ΠΎΡΠΈΠ΅Π½ΡΠΈΡΠΎΠ²Π°Π½Π½ΠΎΠΉ Π²Π΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΠΈ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ // ΠΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΠ΅. — 1986. — N 1. — Π‘. 3−12.
- ΠΠ΅ΠΏΠΎΠΌΠ½ΡΡΠΈΠΉ Π.Π. ΠΠ΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΡ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ Π½Π°Π΄ ΠΌΠ°ΡΡΠΈΠ²Π°ΠΌΠΈ // Π‘ΠΈΡΡΠ΅ΠΌΠ½Π°Ρ ΠΈΠ½ΡΠΎΡΠΌΠ°ΡΠΈΠΊΠ°. — ΠΠΎΠ²ΠΎΡΠΈΠ±ΠΈΡΡΠΊ, 1993. — ΠΡΠΏ. 3. — Π‘. 68—98.
- ΠΠ΅ΠΏΠΎΠΌΠ½ΡΡΠΈΠΉ Π.Π. ΠΠ΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΡ ΡΠΈΠ½ΠΈΡΠ½ΠΎΠΉ ΠΈΡΠ΅ΡΠ°ΡΠΈΠΈ Π½Π°Π΄ Π½Π°Π±ΠΎΡΠ°ΠΌΠΈ ΡΡΡΡΠΊΡΡΡ Π΄Π°Π½Π½ΡΡ // ΠΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΠ΅. — 2002. — N 1. — Π‘. 3−12.
- ΠΠ΅ΠΏΠΎΠΌΠ½ΡΡΠΈΠΉ Π.Π., ΠΠ½ΡΡΠ΅Π΅Π² Π. Π‘., ΠΠΈΡ Π°ΠΉΠ»ΠΎΠ² Π. Π., ΠΡΠΎΠΌΡΠΊΠΈΠΉ Π. Π. ΠΠ° ΠΏΡΡΠΈ ΠΊ Π²Π΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΠΈ Π‘-ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ. Π―Π·ΡΠΊ C-light // ΠΠΎΠ½Ρ., ΠΏΠΎΡΠ²ΡΡΠ΅Π½Π½Π°Ρ 90-Π»Π΅ΡΠΈΡ ΡΠΎ Π΄Π½Ρ ΡΠΎΠΆΠ΄Π΅Π½ΠΈΡ Π. Π. ΠΡΠΏΡΠ½ΠΎΠ²Π° (ΠΏΠ»Π΅Π½Π°ΡΠ½ΡΠ΅ Π΄ΠΎΠΊΠ»Π°Π΄Ρ). — ΠΠΎΠ²ΠΎΡΠΈΠ±ΠΈΡΡΠΊ, 2001. — Π‘. 423−432.
- ΠΠ΅ΠΏΠΎΠΌΠ½ΡΡΠΈΠΉ Π.Π., ΠΠ½ΡΡΠ΅Π΅Π² Π. Π‘., ΠΠΈΡ Π°ΠΉΠ»ΠΎΠ² Π. Π., ΠΡΠΎΠΌΡΠΊΠΈΠΉ Π. Π. ΠΠ° ΠΏΡΡΠΈ ΠΊ Π²Π΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΠΈ Π‘ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ. Π§Π°ΡΡΡ 1. Π―Π·ΡΠΊ C-light. — ΠΠΎΠ²ΠΎΡΠΈΠ±ΠΈΡΡΠΊ, 2001. — 48 Ρ. — (ΠΡΠ΅ΠΏΡ. / Π ΠΠ. Π‘ΠΈΠ±. ΠΡΠ΄-Π½ΠΈΠ΅. ΠΠ‘Π- N 84).
- ΠΠ΅ΠΏΠΎΠΌΠ½ΡΡΠΈΠΉ Π.Π., ΠΠ½ΡΡΠ΅Π΅Π² Π. Π‘., ΠΠΈΡ Π°ΠΉΠ»ΠΎΠ² Π. Π., ΠΡΠΎΠΌΡΠΊΠΈΠΉ Π. Π. ΠΠ° ΠΏΡΡΠΈ ΠΊ Π²Π΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΠΈ Π‘ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ. Π§Π°ΡΡΡ 2. Π―Π·ΡΠΊ C-light-kernel ΠΈ Π΅Π³ΠΎ Π°ΠΊΡΠΈΠΎΠΌΠ°ΡΠΈΡΠ΅ΡΠΊΠ°Ρ ΡΠ΅ΠΌΠ°Π½ΡΠΈΠΊΠ°. — ΠΠΎΠ²ΠΎΡΠΈΠ±ΠΈΡΡΠΊ, 2001. — 58 Ρ. — (ΠΡΠ΅ΠΏΡ. / Π ΠΠ. Π‘ΠΈΠ±. ΠΡΠ΄-Π½ΠΈΠ΅. ΠΠ‘Π- N 87).
- ΠΠ΅ΠΏΠΎΠΌΠ½ΡΡΠΈΠΉ Π.Π., ΠΠ½ΡΡΠ΅Π΅Π² Π. Π‘., ΠΠΈΡ Π°ΠΉΠ»ΠΎΠ² Π. Π., ΠΡΠΎΠΌΡΠΊΠΈΠΉ Π. Π. ΠΠ° ΠΏΡΡΠΈ ΠΊ Π²Π΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΠΈ Π‘ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ. Π§Π°ΡΡΡ 3. ΠΠ΅ΡΠ΅Π²ΠΎΠ΄ ΠΈΠ· ΡΠ·ΡΠΊΠ° C-light Π² ΡΠ·ΡΠΊ C-light-kernel ΠΈ Π΅Π³ΠΎ ΡΠΎΡΠΌΠ°Π»ΡΠ½ΠΎΠ΅ ΠΎΠ±ΠΎΡΠ½ΠΎΠ²Π°Π½ΠΈΠ΅. — ΠΠΎΠ²ΠΎΡΠΈΠ±ΠΈΡΡΠΊ, 2002. — 82 Ρ. — (ΠΡΠ΅ΠΏΡ. / Π ΠΠ. Π‘ΠΈΠ±. ΠΡΠ΄-Π½ΠΈΠ΅. ΠΠ‘Π- N 97).
- ΠΠ΅ΠΏΠΎΠΌΠ½ΡΡΠΈΠΉ Π.Π., ΠΠ½ΡΡΠ΅Π΅Π² Π. Π‘., ΠΠΈΡ Π°ΠΉΠ»ΠΎΠ² Π. Π., ΠΡΠΎΠΌΡΠΊΠΈΠΉ Π. Π. ΠΠ° ΠΏΡΡΠΈ ΠΊ Π²Π΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΠΈ Π‘ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ. Π―Π·ΡΠΊ C-light ΠΈ Π΅Π³ΠΎ ΡΠΎΡΠΌΠ°Π»ΡΠ½Π°Ρ ΡΠ΅ΠΌΠ°Π½ΡΠΈΠΊΠ°. // ΠΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΠ΅. — 2002. — N 6. — Π‘. 1−13.
- ΠΠ΅ΠΏΠΎΠΌΠ½ΡΡΠΈΠΉ Π.Π., ΠΠ½ΡΡΠ΅Π΅Π² Π. Π‘., ΠΠΈΡ Π°ΠΉΠ»ΠΎΠ² Π. Π., ΠΡΠΎΠΌΡΠΊΠΈΠΉ Π. Π. ΠΠ° ΠΏΡΡΠΈ ΠΊ Π²Π΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΠΈ Π‘ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ. ΠΠΊΡΠΈΠΎΠΌΠ°ΡΠΈΡΠ΅ΡΠΊΠ°Ρ ΡΠ΅ΠΌΠ°Π½ΡΠΈΠΊΠ° ΡΠ·ΡΠΊΠ° C-kernel // ΠΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΠ΅. — 2003. — N 6. — Π‘. 1−16.
- ΠΠ΅ΠΏΠΎΠΌΠ½ΡΡΠΈΠΉ Π.Π., Π ΡΠΊΠΈΠ½ Π. Π. ΠΡΠΈΠΊΠ»Π°Π΄Π½ΡΠ΅ ΠΌΠ΅ΡΠΎΠ΄Ρ Π²Π΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΠΈ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ. — Π.: Π Π°Π΄ΠΈΠΎ ΠΈ ΡΠ²ΡΠ·Ρ, 1988. — 256 Ρ.
- ΠΠ΅ΠΏΠΎΠΌΠ½ΡΡΠΈΠΉ Π.Π., Π‘ΡΠ»ΠΈΠΌΠΎΠ² Π. Π. ΠΠ΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΡ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ Π»ΠΈΠ½Π΅ΠΉΠ½ΠΎΠΉ Π°Π»Π³Π΅Π±ΡΡ Π² ΡΠΈΡΡΠ΅ΠΌΠ΅ Π‘ΠΠΠΠ’Π // ΠΠΈΠ±Π΅ΡΠ½Π΅ΡΠΈΠΊΠ° ΠΈ ΡΠΈΡΡΠ΅ΠΌΠ½ΡΠΉ Π°Π½Π°Π»ΠΈΠ·. — 1992. — N 5. — Π‘. 136−144.
- ΠΠ΅ΠΏΠΎΠΌΠ½ΡΡΠΈΠΉ Π.Π., Π‘ΡΠ»ΠΈΠΌΠΎΠ² Π. Π. ΠΡΠΎΠ±Π»Π΅ΠΌΠ½ΠΎ-ΠΎΡΠΈΠ΅Π½ΡΠΈΡΠΎΠ²Π°Π½Π½ΡΠ΅ Π±Π°Π·Ρ Π·Π½Π°Π½ΠΈΠΉ ΠΈ ΠΈΡ ΠΏΡΠΈΠΌΠ΅Π½Π΅Π½ΠΈΠ΅ Π² ΡΠΈΡΡΠ΅ΠΌΠ΅ Π²Π΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΠΈ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ Π‘ΠΠΠΠ’Π // ΠΠ·Π². Π ΠΠ. Π‘Π΅Ρ. «Π’Π΅ΠΎΡΠΈΡ ΠΈ ΡΠΈΡΡΠ΅ΠΌΡ ΡΠΏΡΠ°Π²Π»Π΅Π½ΠΈΡ». — 1997. — N 2. — Π‘. 169−175.
- ΠΠΎΠ΄Π»ΠΎΠ²ΡΠ΅Π½ΠΊΠΎ Π .Π. Π€ΡΠ½ΠΊΡΠΈΠΎΠ½Π°Π»ΡΠ½Π°Ρ ΠΈ Π΄ΡΡΠ³ΠΈΠ΅ ΡΠΊΠ²ΠΈΠ²Π°Π»Π΅Π½ΡΠ½ΠΎΡΡΠΈ ΡΡ Π΅ΠΌ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ //. ΠΡΠΎΠ±Π»Π΅ΠΌΡ ΠΊΠΈΠ±Π΅ΡΠ½Π΅ΡΠΈΠΊΠΈ. — Π.: ΠΠ°ΡΠΊΠ°, 1979. — ΠΡΠΏ. 35. — Π‘. 185−198.
- ΠΡΠ°ΡΡ Π’., ΠΠ΅Π»ΠΊΠΎΠ²ΠΈΡ Π. Π―Π·ΡΠΊΠΈ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΡ: ΡΠ°Π·ΡΠ°Π±ΠΎΡΠΊΠ° ΠΈ ΡΠ΅Π°Π»ΠΈΠ·Π°ΡΠΈΡ (4-Π΅ ΠΈΠ·Π΄.) / ΠΠΎΠ΄ ΠΎΠ±ΡΠ΅ΠΉ ΡΠ΅Π΄. Π. ΠΠ°ΡΡΠΎΡΠΎΠ²Π°. — Π‘ΠΠ±.: ΠΠΈΡΠ΅Ρ, 2002. — 688 Ρ.
- ΠΡΠΎΠΌΡΠΊΠΈΠΉ Π.Π. ΠΠΏΠ΅ΡΠ°ΡΠΈΠΎΠ½Π½Π°Ρ ΠΈ Π°ΠΊΡΠΈΠΎΠΌΠ°ΡΠΈΡΠ΅ΡΠΊΠ°Ρ ΡΠ΅ΠΌΠ°Π½ΡΠΈΠΊΠΈ ΡΠ·ΡΠΊΠ° Π‘ΠΈ // (ΠΠΠΠ ΠΠ-2000): Π’Π΅Π·. Π΄ΠΎΠΊΠ». / Π§Π΅ΡΠ²Π΅ΡΡΡΠΉ ΡΠΈΠ±ΠΈΡΡΠΊΠΈΠΉ ΠΊΠΎΠ½Π³ΡΠ΅ΡΡ ΠΏΠΎ ΠΏΡΠΈΠΊΠ»Π°Π΄Π½ΠΎΠΉ ΠΈ ΠΈΠ½Π΄ΡΡΡΡΠΈΠ°Π»ΡΠ½ΠΎΠΉ ΠΌΠ°ΡΠ΅ΠΌΠ°ΡΠΈΠΊΠ΅. — ΠΠΎΠ²ΠΎΡΠΈΠ±ΠΈΡΡΠΊ, 2000. — Π§. 2. — Π‘. 125.
- ΠΡΠΎΠΌΡΠΊΠΈΠΉ Π.Π. Π€ΠΎΡΠΌΠ°Π»ΡΠ½Π°Ρ ΡΠ΅ΠΌΠ°Π½ΡΠΈΠΊΠ° ΡΠΊΠ°Π·Π°ΡΠ΅Π»Π΅ΠΉ ΡΠ·ΡΠΊΠ° C-light // ΠΠ°ΡΠ΅ΡΠΈΠ°Π»Ρ ΠΊΠΎΠ½Ρ. ΠΌΠΎΠ»ΠΎΠ΄ΡΡ ΡΡΠ΅Π½ΡΡ , ΠΏΠΎΡΠ²ΡΡΠ΅Π½Π½ΠΎΠΉ 10-Π»Π΅ΡΠΈΡ ΠΠ½ΡΡΠΈΡΡΡΠ° Π²ΡΡΠΈΡΠ»ΠΈΡΠ΅Π»ΡΠ½ΡΡ ΡΠ΅Ρ Π½ΠΎΠ»ΠΎΠ³ΠΈΠΉ Π‘Π Π ΠΠ. ΠΠΎΠ²ΠΎΡΠΈΠ±ΠΈΡΡΠΊ, 2001. — Π’. 1. — Π‘. 62−65.
- ΠΡΠΎΠΌΡΠΊΠΈΠΉ Π.Π. ΠΠ²ΡΠΎΠΌΠ°ΡΠΈΡΠ΅ΡΠΊΠ°Ρ Π³Π΅Π½Π΅ΡΠ°ΡΠΈΡ ΡΡΠ»ΠΎΠ²ΠΈΠΉ ΠΊΠΎΡΡΠ΅ΠΊΡΠ½ΠΎΡΡΠΈ Π² ΡΠΈΡΡΠ΅ΠΌΠ΅ Π²Π΅ΡΠΈΡΠΈΠΊΠ°ΡΠΈΠΈ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌ // Π’Π΅Π·. Π΄ΠΎΠΊΠ». ΠΌΠ΅ΠΆΠ΄ΡΠ½Π°Ρ. ΠΊΠΎΠ½Ρ. ΠΌΠΎΠ»ΠΎΠ΄ΡΡ ΡΡΠ΅Π½ΡΡ ΠΏΠΎ ΠΌΠ°ΡΠ΅ΠΌΠ°ΡΠΈΡΠ΅ΡΠΊΠΎΠΌΡ ΠΌΠΎΠ΄Π΅Π»ΠΈΡΠΎΠ²Π°Π½ΠΈΡ ΠΈ ΠΈΠ½ΡΠΎΡΠΌΠ°ΡΠΈΠΊΠ΅. — ΠΠΎΠ²ΠΎΡΠΈΠ±ΠΈΡΡΠΊ, 2002. — Π‘. 67.
- ΠΡΠΎΠΌΡΠΊΠΈΠΉ Π.Π. ΠΠ΅Π½Π΅ΡΠ°ΡΠΈΡ ΠΈ ΠΌΠ΅ΡΠ°Π³Π΅Π½Π΅ΡΠ°ΡΠΈΡ ΡΡΠ»ΠΎΠ²ΠΈΠΉ ΠΊΠΎΡΡΠ΅ΠΊΡΠ½ΠΎΡΡΠΈ Π² ΡΠΈΡΡΠ΅ΠΌΠ΅ Π‘ΠΠΠΠ’Π -2. ΠΠΎΠ²ΠΎΡΠΈΠ±ΠΈΡΡΠΊ, 2003. — 50 Ρ. — (ΠΡΠ΅ΠΏΡ. / Π ΠΠ. Π‘ΠΈΠ±. ΠΡΠ΄-Π½ΠΈΠ΅. ΠΠ‘Π- N 103).
- Π₯ΡΠ·ΡΠΈΠ»Π΄ Π ., ΠΠΈΡΠ±ΠΈ JL, ΠΈ Π΄Ρ. ΠΡΠΊΡΡΡΠ²ΠΎ ΠΏΡΠΎΠ³ΡΠ°ΠΌΠΌΠΈΡΠΎΠ²Π°Π½ΠΈΡ Π½Π° Π‘. Π€ΡΠ½Π΄Π°ΠΌΠ΅Π½ΡΠ°Π»ΡΠ½ΡΠ΅ Π°Π»Π³ΠΎΡΠΈΡΠΌΡ, ΡΡΡΡΠΊΡΡΡΡ Π΄Π°Π½Π½ΡΡ ΠΈ ΠΏΡΠΈΠΌΠ΅ΡΡ ΠΏΡΠΈΠ»ΠΎΠΆΠ΅Π½ΠΈΠΉ. — Π.: ΠΠΈΠ°Π‘ΠΎΡΡ, 2001. 736 Ρ.
- Andersen L.O. Program analysis and specialization for the Π‘ programming language. Thes. doct. phylosophy (computer sci.). — DIKU, Universisty of Copenhagen, 1994. — (DIKU report 94/19).
- Apt K.R. Ten years of Hoare’s logic: A survey — Part I // ACM Trans. Progr. Lang, and Systems. 1981. — Vol. 3, N. 4. — P. 431−483.
- Apt K.R., Olderog E.R. Verification of sequential and concurrent programs. — Berlin etc.: Springer, 1991. — 450 p.
- Arbib M.A., Alagic S. Proof rules for Gotos // Acta Informatica. 1979. — N 11, -P. 139−148.
- Archer M., Lo A., Olsson R.A. Towards a transformational approach to program verification. // Software Testing, Verification & Reliability. — 1999. — Vol. 9, N 2, — P. 85−106.
- Ball Π’., Rajamani S.K.The SLAM project: debugging a system via static analysis // POPL 2002. URL: http://research.microsoft.com/slam.
- Bensalem S., Lakhnech Y., Saidi H. Powerful techniques for the automatic generation of invariants. // Lect. Notes Comput. Sci. — Berlin etc., 1996. — Vol. 1102. — P. 323−335.
- Bergstra J.A., Tucker J.V. Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs. — Amsterdam, 1980. — (Rep. / Mathematisch Centrum- IW 136/80).
- Bergstra J.A., Tucker J.V. Expressiveness and the completeness of Hoare’s logic. — Amsterdam, 1980. — (Rep. / Mathematisch Centrum- IW 149/80).
- Black P.E. Axiomatic semantics verification of a secure Web server: Thes. doct. phylosophy (computer sci.). — Brigham Young Universisty, 1998. — 255 p.
- Black P.E., Windley Ph.J. Inference rules for programming languages with side effects in expressions // Lect. Notes Comput. Sci. — Berlin etc., 1996. — Vol. 1125. — P. 56−60.
- Black P.E., Windley Ph.J. Formal verification of programs in the presence of side effects // Proc. 31st Annual Hawai’i Intern. Conf. on System Science. — IEEE Computer Science Press. 1998. — Vol. 3. — P. 327−334.
- Blass A., Gurevich Y. Inadequacy of computable loop invariants. // ACM Trans. Computational Logic. — 2001. — Vol. 2, Issue 1. — P. 1−11.
- Boekhold M., Karkowski I., Corporaal H., Cilio A. A programmable ANSI Π‘ code transformation engine. — Delft, 1998. — (Tech. Rep. / Delft University of Technology- N l-68 340−44(1998)-08).
- Bofinger M. Reasoning about Π‘ programs: Thes. doct. phylosophy (computer sci.). — University of Queensland, 1998.
- Bornat R. Proving pointer programs in Hoare logic // Lect. Notes Comput. Sci. — Berlin etc, 2000. Vol. 1873. — P. 102−126.56. de Bruin A. Goto statements: semantics and deduction systems // Acta Informatica.- 1981. — N 15. — 385−424.
- Calcagno C., Ishtiaq S., O’Hearn P.W. Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic // Proc. ACM-SIGPLAN 2nd Intern. Conf. Principles and Practice of Declarative Programming. — ACM Press, 2000. — 32 p.
- Cannon L.W., Elliott R.A., Kirchhoff L.W., Miller J.H., Milner J.M., Mitze R.W., Schan E.P., Whittington N.O., Spencer H., Keppel D., Brader M.
- Recommended Π‘ style and coding standards. — 2000. URL: http: //sunland. gsf Ρ.nasa. gov/inf o/cstyle. html.
- Cattel T. Modelling and verificarion of sC++ applications // Lect. Notes Comput. Sci.- Berlin etc, 1998. Vol. 1384. — P. 232−248.
- Chaki S., Clarke E., Groce A., Jha S., Veith H. Modular verification of software components in Π‘ // Proc. 25th Intern. Conf. Software Eng. — IEEE Computer Society, 2003. P. 385−395.
- Chandra A.K., Manna Z. Program schemes with equality // Proc. 4th Ann. ACM Symp. on Theory Π‘ΠΎΡΡ. — Denver, 1972. — P. 52−64.
- Clarke E. Completeness and incompleteness theorems for Hoare-like axiom systems: Thes. doct. phylosophy (computer sci.). — Cornell Univ., Computer Science Dep., 1976.
- Clarke E. Programming language constructs for which it is impossible to obtain good Hoare axiom systems //J. Assoc. Computing Machinery. — 1979. — Vol. 26, N 1. — P. 129−147.
- Clarke E., Kroening D. Hardware verification using ANSI-C programs as a reference // Proc. ASP-DAC 2003. IEEE Computer Society Press, 2003. — P. 308−311.
- Clarke E., Kroening D., Yorav K. Behavioral consistency of Π‘ and Verilog programs using Bounded Model Checking. — Pittsburgh, 2003. — (Technical Rep. / Carnegie Mellon Univ., School of Computer Science- CMU-CS-03−126).
- Clarke E., Kroening D., Sharygina N., Yorav K. Predicate Abstraction of ANSI-C Programs using SAT // Proc. Model Checking for Dependable Software-Intensive Systems Workshop, San-Francisco, USA, 2003.
- URL: http: //www-2. cs. emu.edu/~svc/papers/.
- Clarke E., Kroening D., Lerda F. A tool for checking ANSI-C programs // Lect. Notes Comput. Sci. Berlin etc, 2004. — Vol. 2988. — P. 158−176.
- Clint M., Hoare C.A.R. Program proving: jumps and functions // Acta Informatica.- 1972. — N 1. P. 214−224.
- Cook S.A. Soundness and completeness of an axiom system for program verification // SIAM J. Computing. 1978. — Vol. 7, N 1. — P. 70−90.
- Cousot P. Methods and logics for proving programs // Handbook of Theoretical Computer Science, vol. Π (Formal Models and Semantics), Ch. 15. — Elsevier, 1990.- P. 843−993.
- Cousot P. Abstract interpretation based formal methods and future challenges // Lect. Notes Comput. Sci. Berlin etc, 2001. — Vol. 2000. — P. 138−156.
- Dolado J.J., Harman M., Otero M.C. An empirical investigation of the influence of a type of side effects on program comprehension // IEEE Trans. Software Eng. — 2004.- Vol. 29, N. 7. P. 665−670.
- DuVarney D.C., Purushothaman Iyer S. Π‘ Wolf — a toolset for extracting models from Π‘ programs // Proc. / IFIP WG 6.1 22nd Intern. Conf. Formal Techniques for Networked and Distributed Systems. — London, 2002. P. 260−275.
- Elgaard J., Moller A., Schwartzbach M.I. Compile-time debugging of Π‘ programs working on trees // Lect. Notes Comput. Sci. Berlin etc., 2000. — Vol. 1782. — P. 119−134.
- Floyd R. W. Assigning meanings to programs // Proc. AMS Symp. Applied Mathematics. — American Mathematical Society, Providence, R.I., 1967. — Vol. 19. — P. 19−31.
- Fradet P., Gaugne R., Le Metayer D. Static detection of pointer errors: an axiomatisation and a checking algorithm // Lect. Notes Comput. Sci. — Berlin etc., 1996. Vol. 1058. — P. 125−140.
- Fraer R. Tracing the origins of verification conditions. — Rocquencourt, 1996. — 17 p.- (Rapp. / INRIA- N 2840).
- Gerhart S.L. An overview of AFFFIRM: a specification and verification system // Proc. IFIP Congress (Tokyo, Melbourne, 1980). Amsterdam, 1980. — P. 343−347.
- Gribomont E.P. Simplification of Boolean verification conditions. — Liege, 1999. — 25 p. — (Prepr. / Institut Montefiore, Universite de Liege).
- Gries D. The multiple assignment statement // IEEE Trans. Software Eng. — 1978. — Vol. SE-4, N 6. — P. 89−93.
- Gries D., Levin G. Assignment and procedure call proof rules // ACM Trans. Progr. Lang, and Systems. 1980. — Vol. 2, N 4. — P. 564−579.
- Guidelines for the Use of the Π‘ Language in Vehicle Based Software. The Motor Industry Software Reliability Association, 1998. URL: http://www.misra.org.uk.
- Gurevich Y., Huggins J.Π. The semantics of the Π‘ programming language // Lect. Notes Comput. Sci. Berlin etc., 1993. — Vol. 702. — P. 274−309.
- Hailpern Π., Santhanam P. Software debugging, testing, and verification // IBM Systems J. 2002. — Vol. 41, N 1. — P. 4−12.
- Harman M., Hu L., Munro M., Zhang X. Side-effect removal transformation // Proc. IEEE Int’l Workshop Program Comprehension. — IEEE Computer Society Press, 2001. P. 310−319.
- Harman M., Hu L., Munro M., Zhang X. Weakest precondition for general recursive programs formalized in Coq // Lect. Notes Comput. Sci. — Berlin etc., 2002. — Vol. 2410. P. 332−348.
- Harman M., Hu L., Hierons R., Wegener J., Sthamer H., Baresel A., Roper
- M. Testability transformation // IEEE Trans Software Eng. 2004. — N 30(1). — P. 3−16.
- Haugh E.D. Testing Π‘ programs for buffer overflow vulnerabilities: Thes. master of science. — Univ. of California, Davis. 1999. — 82 p.
- Heintze N., Tardieu O. Ultra-fast aliasing analysis using CLA: a million lines of Π‘ code in a second // Proc. ACM SIGPLAN 2001 conf. Programming language design and implementation. ACM Press, 2001. — P. 254−263.
- Hoare C.A.R. An axiomatic basis for computer programming // Communs ACM. — 1969. Vol. 12, N 1. — P. 576−580.
- Hoare C.A.R. Assertions / Proc. of the NATO Advanced Study Inst, on Models, Algebras and Logic of Engineering Software, Marktoberdorf, Germany, July 30 August 11, 2002. — Amsterdam, 2003. — P. 291−316.
- Hoare C.A.R., Jifeng H. A trace model for pointers and objects // Lect. Notes Comput. Sci. Berlin etc., 1999. — Vol. 1628. — P. 1−18.
- Hoare C.A.R., Wirth N. An axiomatic definition of the programming language Pascal // Acta Informatica. 1973. — Vol. 2, N 4. — P. 335−355.
- Hohmuth M., Tews H. The semantics of Π‘++ data types: towards verifying low-level system components // Emerging Trends: Proc. / TPHOLs 2003. — P. 127−144.
- URL: http: //wwwtcs. inf. tu-dresden. de/~tews/science.html. en.
- Holzmann G.J. Logic verification of ANSI Π‘ code with SPIN // Lect. Notes Comput. Sci. Berlin etc., 2000. — Vol. 1885. — P. 131−147.
- Homeier P.V., Martin D.F. Trustworthy tools for trustworthy programs: A verified verification condition generator // Lect. Notes Comput. Sci. — Berlin etc., 1994. — Vol. 859. P. 269−284.
- Homeier P.V., Martin D.F. Mechanical verification of mutually recursive procedures // Lect. Notes Comput. Sci. Berlin etc., 1996. — Vol. 1104. — P. 201−215.
- Huggins J.K., Shen W. The static and dynamic semantics of Π‘ (extended abstract) // Local Proc. Int. Workshop on Abstract State Machines. — Zurich, 2000. — P. 272−284. (ETH TIK-Rep.- N 87).
- Huisman M., Jacobs B. Java program verification via Hoare logic with abrupt termination // Lect. Notes Comput. Sci. — Berlin etc, 2000. — Vol. 1783. — P. 284 303.
- Igarashi S., London R.L., Luckham D.C. Automatic program verification I: A logical basis and its implementation // Acta Informatica. — 1975. — Vol. 4. — P. 145−182.
- ISO commitee JTC/SC22/WG14. Record of responses. URL: ftp: //ftp. dmk. com/DMK/sc22wgl4/RR/.
- Jim Π’., Morrisett G., Grossman D., Hicks M., Cheney J., Wang Y. Cyclone: a safe dialect of Π‘ //In USENIX Annual Technical conf., Monterey, CA, June 2002. URL: http://www.cs.cornell.edu/projects/cyclone.
- Johnson S.C. Lint, Π° Π‘ program checker. 1977. — (Tech. Rep. AT&T Bell Laboratories- N CSTR-65). — updated version TM 78−1273−3.
- Jones R.W.M., Kelly P.H.J. Backwards-compatible bounds checking for arrays and pointers in Π‘ programs // Automated and Algorithmic Debugging. — 1997. — P. 13−26. URL: http: //www-dse. doc. ic. ac. uk/~r j 3/.
- Kleymann T. Hoare logic and VDM: machine-checked soundness and completeness proofs: Thes. doct. phylosophy (computer sci.). — Univ. of Edinburgh, 1998. — 260 p.
- Kleymann T. Hoare logic and auxiliary variables // Formal Aspects of Computing. — 1999. Vol. 11. — P. 541−566.
- Kowaltowski T. Axiomatic approach to side effects and general jumps // Acta Informatica. 1977. — N 7. — P. 357−360.
- Kozen D., Tiuryn J. On the completeness of propositional Hoare logic // Information Sciences. — 2001. Vol. 139, N 3−4. — P. 187−195.
- Kroening D. Application specific higher order logic theorem proving // Proc. Verification Workshop (VERIFY'02). 2002. — P. 5−15.
- Lamport L., Paulson L.C. Should your Specification language be typed? // ACM Trans. Progr. Lang., and Systems. — 1999. — Vol. 8, N. 1. — P. 1−25.
- Lifschitz V. On verification of programs with goto statements // Inform. Processing Letters. 1984. — N 18. — P. 221−225.
- Lipton R.J. A necessary and sufficient condition for the existence of Hoare Logics //In Proc. 18th IEEE Symp. Foundations of Computer Sci. — 1977. P. 1−6.
- London R.I. et al. Proof rules for the programming language EUCLID // Acta Informatica. 1978. — Vol. 10. — P. 1−26.
- Luckham D.C., Suzuki N. Verification of array, record and pointer operations in Pascal // ACM Trans. Progr. Lang., and Systems. 1979. — Vol. 1, N 2. — P. 226−244.
- Manna Z., Waldinger R. Problematic features of programming languages: A situational-calculus approach // Acta Informatica. — 1981. — Vol. 16, N 4. — P. 371−426.
- McCarthy J. Towards a mathematical science of computation // Proc. IFIP Congress 62. Amsterdam, 1962. — P. 21−28.
- Meyer B. Object-oriented software construction (2nd ed.). — Prentice Hall PTR, 1997.
- Milner R. Equivalences on program schemes //J. Computer and System Sci. — 1970. Vol. 4, N. 3. — P. 205−219.
- Milner R., Tofte M., Harper R.W. The definition of Standard ML. MIT Press, 1990.
- Moore J. S. Proving theorems about Java and the JVM with ACL2 / Proc. of the NATO Advanced Study Inst, on Models, Algebras and Logic of Engineering Software, Marktoberdorf, Germany, July 30 August 11, 2002. — Amsterdam, 2003. — P. 227−290.
- Moriconi M., Schwartz R.L. Automatic construction of cerification condition generators from Hoare logics // Lect. Notes Comput. Sci. — Berlin etc., 1981. — Vol. 115. P. 363−377.
- Muller-Olm M., Wolf A. On Excusable and inexcusable failures: Towards an adequate notion of translation correctness // Lect. Notes Comput. Sci. — Berlin etc, 1999. — Vol. 1709. P. 1107−1126.
- Muller-Olm M., Seidl H. Computing polynomial program invariants// Inform. Processing Letters. 2004. — N 91(5). — P. 233−244.
- Nepomniaschy V.A. On a symbolic method of verification for definite iteration over data structures / / Joint Bulletin of the Institute of Informatics Systems and Computer Center. 1998. — N 5. — P. 1−22.
- Nepomniaschy V.A. Verification of pointer programs using symbolic method for definite iterations // Joint Bulletin of the Institute of Informatics Systems and Computer Center. 2000. — N 13. — P. 56−66.
- Nepomniaschy V.A. Symbolic verification method for definite iterations over tuples of. data structures // Joint Bulletin of the Institute of Informatics Systems and Computer Center. 2001. — N 15. — P. 103−123.
- Nepomniaschy V.A., Sulimov A.A. Problem-Oriented Means of Program Specification and Verification in Project SPECTRUM // Lect. Notes Comput. Sci. — 1993. Vol. 722. — P. 374−378.
- Nepomniaschy V.A., Sulimov A.A. Towards Automatic Program Verification: Problem-Oriented Knowledge Bases // Specification, verification and net models of concurrent systems. — Novosibirsk, 1994. — P. 138—150.
- Nimmer J.W., Ernst M.D. Automatic generation of program specifications. Nimmer, J.W., Ernst, M.D.: Automatic generation of program specifications // Proc. international symposium on Software testing and analysis. — ACM Press, 2002. — P. 229−240.
- Nipkow T. Hoare logics for recursive procedures and unbounded nondeterminism.2001. — (Draft / Fakultat fur Informatik, Technische Universitat Munchen). URL: http://www.in.turn.de/~nipkow/.
- Norrish M. Derivation of verification rules for Π‘ from operational definitions // Supplementary Proc. 9th International Conf. Theorem Proving in Higher Order Logics.- TUCS General Publication N 1, Turku Centre for Computer Science, 1996. — P. 69−75.
- Norrish M. Π‘ formalised in HOL: Thes. doct. phylosophy (computer sci.). — Cambridge, 1998. 150 p.
- Norrish M. Deterministic expressions in Π‘ // Lect. Notes Comput. Sci. — Berlin etc, 1999. — Vol. 1576. P. 147−161.
- O’Donnell M.J. A critique of the foundations of Hoare style programming logics // Communs ACM. 1982. — Vol. 25, N 12. — P. 927−935.
- Oheimb D. von. Hoare logic for mutual recursion and local variables // Lect. Notes Comput. Sci. Berlin etc., 1999. — Vol. 1738. — P. 168−180.
- Oheimb D. von. Hoare logic for Java in Isabelle/HOL // Concurrency and Computation: Practice and Experience, 13(13), 2001.
- URL: http: //isabelle. in. turn. de/Bali/papers/CPEOl.html.
- Oheimb D. von, Nipkow T. Hoare logic for NanoJava: auxiliary variables, side effects, and virtual methods revisited // Lect. Notes Comput. Sci. — Berlin etc., 2002. — Vol. 2391. P. 89−105.
- Owre S., Rushby J., Shankar N. PVS: A prototype verification system // Lect. Notes Art. Intell. 1992. — Vol. 607. — P. 748−752.
- Paraspyrou N.S. A formal semantics for the Π‘ programming language: Thes. doct. phylosophy (computer sci.). — National Technical University of Athens, 1998. — 269 p.
- Paraspyrou N.S., Maco§ D. A study of evaluation order semantics in expressions with side effects // J. Functional Programming. — 2000. — N 10(3), — P. 227−244.
- Paraspyrou N.S., Vescoukis V.C. Facilitating the definition of programming languages by using parametric context-free grammars // Advances in Informatics. — 2000. P. 260−272.
- Plotkin G.D. A structure approach to operational semantics. — 1981. — (Tech. Rep./ DAIMI/Aarhus University- FN-19).
- Plotkin G.D. The origins of structural operational semantics // Inform. Processing Letters. — 2003. Vol. 88, Issue 1−2. — P. 27−32.
- Poetzsch-Heffer A., Mtiller P. A programming logic for sequential Java // Lect. Notes Comput. Sci. Berlin etc., 1999. — Vol. 1576. — P. 162−176.
- Programming languages C: ISO/IEC 9899:1990. — 1990.
- Programming languages C: ISO/IEC 9899:1999. — 1999. — 566 p.
- Reynolds J.C. Theories of Programming Languages. — Cambridge University Press, 1998. 500 p.
- Ritchie D.M. The developement of the Π‘ language //In 2nd History of Programming Languages conf., Cambridge, Mass., — ACM, 1993.
- Scott D.S., Strachey C. Towards a mathematical semantics for programming languages. — Oxford, 1971. — (Tech. Rep. / Programmnig Research Group, University of Oxford- N PRG-6).
- Sharma Π., Dhodapkar S.D., Ramesh S. Assertion checking environment (ACE) for formal verification of Π‘ programs // Lect. Notes Comput. Sci. — Berlin etc., 2002. — Vol. 2434. P. 284−295.
- Simon A., King A. Analysing string buffers in C. — Kent, 2002. — (Tech. Rep. / Computing Laboratory, Univ. of Kent- N 2−02).
- Stoy J.E. Denotational semantics: the Scott-Strachey approach to programmnig language theory. — MIT Press, Cambridge, Mass., 1977.
- Subramanian S., Cook J.V. Machanichal verification of Π‘ programs // In 1st workshop on Formal Methods in Software Practice (FMSP1996). — J. Assoc. Computing Machinery, 1996.
- Suzuki N. Automatic verification of programs with complex data structure: Thes. doct. phylosophy (computer sci.). — Stanford Univ., 1976.
- Suzuki N. Analysis of pointer Rotation // Communs ACM. — 1982. — Vol. 25, Issue 5. P. 330−335.
- US National Institute of Standards and Technology. The Economic Impacts of Inadequate Infrastructure for Software Testing, May 2002.
- Wand M. A new incompleteness result for Hoare’s system //J. Assoc. Computing Machinery. 1978. — Vol. 25, N 1. — P. 168−175.
- Wang C., Musser D.R. Dynamic verification of Π‘++ generic algorithms // IEEE Trans. Software Eng. 1997. — Vol. 23, N 5. — P. 314−322.
- Wilson R.P., Lam M.S. Efficient context-sensitive pointer analysis for Π‘ programs // ACM SIGPLAN Notices. 1995. — Vol. 30, N 6. — P. 1−12.
- Zamulin A.V. Algebraic modelling of imperative languages with pointers // Lect. Notes Comput. Sci. Berlin etc., 1993. — Vol. 735. — P. 81−97.