Sign In

Combining Mechanical and Agentic Specification Inference for Move

์ž‘์„ฑ์ž
  • Haebom
์นดํ…Œ๊ณ ๋ฆฌ
Empty

์ €์ž

Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap

๐Ÿ’ก ๊ฐœ์š”

๋ณธ ๋…ผ๋ฌธ์€ Move Prover๋ฅผ ์œ„ํ•œ ๋ช…์„ธ ์ถ”๋ก  ๋„๊ตฌ๋ฅผ ์ œ์•ˆํ•ฉ๋‹ˆ๋‹ค. ์ด ๋„๊ตฌ๋Š” Move ๋ฐ”์ดํŠธ์ฝ”๋“œ์— ๋Œ€ํ•œ ์•ฝํ•œ ์‚ฌ์ „์กฐ๊ฑด(WP) ๋ถ„์„๊ณผ Claude Code์™€ ๊ฐ™์€ ์—์ด์ „ํŠธ ๊ธฐ๋ฐ˜ ์ฝ”๋”ฉ CLI๋ฅผ ๊ฒฐํ•ฉํ•˜์—ฌ, ๋ฐ˜๋ณต์ ์ธ ๋ช…์„ธ ์ž‘์„ฑ ๊ณผ์ •์„ ์ž๋™ํ™”ํ•ฉ๋‹ˆ๋‹ค. WP ๋ถ„์„์€ ๊ธฐ๊ณ„์ ์ธ ๊ธฐ๋ฐ˜์„ ์ œ๊ณตํ•˜๋ฉฐ, AI๋Š” ๋ฃจํ”„ ๋ถˆ๋ณ€์‹, ๋‹จ์กฐ์„ฑ, ๋ณด์กด์„ฑ ๋“ฑ WP๊ฐ€ ์ทจ์•ฝํ•œ ๋ถ€๋ถ„์„ ๋ณด๊ฐ•ํ•˜์—ฌ ์œ ํšจํ•œ ๋ช…์„ธ๋ฅผ ์ƒ์„ฑํ•ฉ๋‹ˆ๋‹ค.

๐Ÿ”‘ ์‹œ์‚ฌ์  ๋ฐ ํ•œ๊ณ„

โ€ข
Move ์–ธ์–ด์˜ ๋ณต์žกํ•œ ์ฝ”๋“œ ๊ฒ€์ฆ์„ ์œ„ํ•œ ๋ช…์„ธ ์ž‘์„ฑ์˜ ๋ฒˆ๊ฑฐ๋กœ์›€์„ ํฌ๊ฒŒ ์ค„์ผ ์ˆ˜ ์žˆ์Šต๋‹ˆ๋‹ค.
โ€ข
๊ธฐ๊ณ„์ ์ธ ๋ถ„์„๊ณผ AI ๊ธฐ๋ฐ˜ ์ถ”๋ก ์„ ๊ฒฐํ•ฉํ•˜์—ฌ ๋ณด๋‹ค ์ •ํ™•ํ•˜๊ณ  ํšจ๊ณผ์ ์ธ ๋ช…์„ธ ์ถ”๋ก ์ด ๊ฐ€๋Šฅํ•ฉ๋‹ˆ๋‹ค.
โ€ข
๊ณ ์ฐจ ํ•จ์ˆ˜, ๋™์  ๋””์ŠคํŒจ์น˜, ์ „์—ญ ์ƒํƒœ, ์ฐธ์กฐ, ๋‹ค์–‘ํ•œ ํ˜•ํƒœ์˜ ๋ฃจํ”„๋ฅผ ํฌํ•จํ•˜๋Š” ๋ฐฉ๋Œ€ํ•œ Move ์ฝ”๋“œ์— ๋Œ€ํ•œ ์ ์šฉ ๊ฐ€๋Šฅ์„ฑ์„ ๋ณด์—ฌ์ค๋‹ˆ๋‹ค.
โ€ข
์ดˆ๊ธฐ ์—ฐ๊ตฌ ๋‹จ๊ณ„์ด๋ฏ€๋กœ, ์ถ”๋ก ๋œ ๋ช…์„ธ์˜ ์™„์„ฑ๋„ ๋ฐ ๋ณต์žกํ•œ ํ”„๋กœ๊ทธ๋žจ์— ๋Œ€ํ•œ ํ™•์žฅ์„ฑ ๋“ฑ ์ถ”๊ฐ€์ ์ธ ์—ฐ๊ตฌ์™€ ๊ฐœ์„ ์ด ํ•„์š”ํ•ฉ๋‹ˆ๋‹ค.
๐Ÿ‘
Made with Slashpage